open import Cat.Functor.Adjoint.Compose
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 be categories displayed over resp. Furthermore, let and be a pair of adjoint functors. We say 2 displayed functors over and resp. are displayed adjoint functors if we have displayed natural transformations and 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 and be categories displayed over some We say that a pair of vertical fibred functors are fibred adjoint functors if they are displayed adjoint functors, and the unit and counit are vertical natural transformations.

Unlike vertical functors and vertical natural transformations, we have to define fibred adjunctions as a separate type: general displayed adjunctions use composition of displayed functors for the unit and counit, whereas fibred adjunctions use vertical composition instead.

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-functor

    lvl : Level
    lvl = ob βŠ” β„“b βŠ” oe βŠ” β„“e βŠ” of βŠ” β„“f

  infix 15 _βŠ£β†“_
  record _βŠ£β†“_
    (L : Vertical-functor β„° β„±)
    (R : Vertical-functor β„± β„°)
    : Type lvl where
    no-eta-equality
    field
      unit' : Id' =>↓ R ∘V L
      counit' : L ∘V R =>↓ Id'

    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'