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′