open import Cat.Functor.Equivalence
open import Cat.Displayed.Functor
open import Cat.Instances.Functor
open import Cat.Displayed.Base
open import Cat.Prelude

module Cat.Displayed.Adjoint where


Following the general theme of defining displayed structure over 1-categorical structure, we can define a notion of displayed adjoint functors.

Let $\mathcal{E}, \mathcal{F}$ be categories displayed over $\mathcal{A}, \mathcal{B}$, resp. Furthermore, let $L : \mathcal{A} \to \mathcal{B}$ and $R : \mathcal{B} \to \mathcal{B}$ be a pair of adjoint functors. We say 2 displayed functors $L', R'$ over $L$ and $R$ resp. are displayed adjoint functors if we have displayed natural transformations $\eta' : \mathrm{Id} \to R' \circ L'$ and $\varepsilon' : L' \circ R' \to \mathrm{Id}$ displayed over the unit and counit of the adjunction in the base that satisfy the usual triangle identities.

module _
{oa βa ob βb oe βe of βf}
{A : Precategory oa βa} {B : Precategory ob βb}
{β° : Displayed A oe βe} {β± : Displayed B of βf}
{L : Functor A B} {R : Functor B A}
where
private
module β° = Displayed β°
module β± = Displayed β±
open Displayed-functor

lvl : Level
lvl = oa β βa β ob β βb β oe β βe β of β βf

infix 15 _β£[_]_

  record _β£[_]_
(L' : Displayed-functor β° β± L)
(R' : Displayed-functor β± β° R )
: Type lvl where
no-eta-equality
field
unit' : Id' =[ unit ]=> R' Fβ' L'
counit' : L' Fβ' R' =[ counit ]=> Id'

module unit' = _=[_]=>_ unit'
module counit' = _=[_]=>_ counit' renaming (Ξ·' to Ξ΅')

field
zig' : β {x} {x' : β°.Ob[ x ]}
β (counit'.Ξ΅' (L' .Fβ' x') β±.β' L' .Fβ' (unit'.Ξ·' x')) β±.β‘[ zig ] β±.id'
zag' : β {x} {x' : β±.Ob[ x ]}
β (R' .Fβ' (counit'.Ξ΅' x') β°.β' unit'.Ξ·' (R' .Fβ' x')) β°.β‘[ zag ] β°.id'


Let $\mathcal{E}$ and $\mathcal{F}$ be categories displayed over some $\mathcal{B}$. We say that a pair of vertical fibred functors $L : \mathcal{E} \to \mathcal{F}$, $R : \mathcal{F} \to cF$ are fibred adjoint functors if they are displayed adjoint functors, and the unit and counit are vertical natural transformations.

module _
{ob βb oe βe of βf}
{B : Precategory ob βb}
{β° : Displayed B oe βe}
{β± : Displayed B of βf}
where
private
open Precategory B
module β° = Displayed β°
module β± = Displayed β±
open Vertical-fibred-functor

lvl : Level
lvl = ob β βb β oe β βe β of β βf

infix 15 _β£β_

  record _β£β_
(L : Vertical-fibred-functor β° β±)
(R : Vertical-fibred-functor β± β°)
: Type lvl where
no-eta-equality
field
unit' : IdVf =>fβ R Vfβ L
counit' : L Vfβ R =>fβ IdVf

module unit' = _=>β_ unit'
module counit' = _=>β_ counit' renaming (Ξ·' to Ξ΅')

field
zig' : β {x} {x' : β°.Ob[ x ]}
β counit'.Ξ΅' (L .Fβ' x') β±.β' L .Fβ' (unit'.Ξ·' x') β±.β‘[ idl id ] β±.id'
zag' : β {x} {x' : β±.Ob[ x ]}
β R .Fβ' (counit'.Ξ΅' x') β°.β' unit'.Ξ·' (R .Fβ' x') β°.β‘[ idl id ] β°.id'