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.

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'