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'