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β²