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

module Cat.Displayed.Adjoint where

Displayed adjunctionsπŸ”—

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

Let E,F\mathcal{E}, \mathcal{F} be categories displayed over A,B\mathcal{A}, \mathcal{B}, resp. Furthermore, let L:Aβ†’BL : \mathcal{A} \to \mathcal{B} and R:Bβ†’BR : \mathcal{B} \to \mathcal{B} be a pair of adjoint functors. We say 2 displayed functors Lβ€²,Rβ€²L', R' over LL and RR resp. are displayed adjoint functors if we have displayed natural transformations Ξ·β€²:Idβ†’Rβ€²βˆ˜Lβ€²\eta' : \mathrm{Id} \to R' \circ L' and Ξ΅β€²:Lβ€²βˆ˜Rβ€²β†’Id\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)
    (adj : L ⊣ R)
    (R' : Displayed-functor β„± β„° R )
    : Type lvl where
    no-eta-equality
    open _⊣_ adj
    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'

Fibred adjunctionsπŸ”—

Let E\mathcal{E} and F\mathcal{F} be categories displayed over some B\mathcal{B}. We say that a pair of vertical fibred functors L:E→FL : \mathcal{E} \to \mathcal{F}, R:F→cFR : \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'