open import Cat.Displayed.Cartesian open import Cat.Displayed.Base open import Cat.Prelude import Cat.Reasoning as CR module Cat.Displayed.Functor where
Displayed and fibred functorsπ
If you have a pair of categories displayed over a common base category , it makes immediate sense to talk about functors : youβd have an assignment of objects and an assignment of morphisms
which makes sense because lies over , just as did, that a morphism is allowed to lie over a morphism . But, in the spirit of relativising category theory, it makes more sense to consider functors between categories displayed over different bases, as in
with our displayed functor lying over an ordinary functor to mediate between the bases.
record Displayed-functor : Type lvl where field Fββ² : β {x} (o : β°.Ob[ x ]) β β±.Ob[ F.β x ] Fββ² : β {a b} {f : A.Hom a b} {aβ² bβ²} β β°.Hom[ f ] aβ² bβ² β β±.Hom[ F.β f ] (Fββ² aβ²) (Fββ² bβ²)
In order to state the displayed functoriality laws, we require functoriality for our mediating functor . Functors between categories displayed over the same base can be recovered as the βvertical displayed functorsβ, i.e., those lying over the identity functor.
F-idβ² : β {x} {o : β°.Ob[ x ]} β PathP (Ξ» i β β±.Hom[ F.F-id i ] (Fββ² o) (Fββ² o)) (Fββ² β°.idβ²) β±.idβ² F-ββ² : β {a b c} {f : A.Hom b c} {g : A.Hom a b} {aβ² bβ² cβ²} {fβ² : β°.Hom[ f ] bβ² cβ²} {gβ² : β°.Hom[ g ] aβ² bβ²} β PathP (Ξ» i β β±.Hom[ F.F-β f g i ] (Fββ² aβ²) (Fββ² cβ²)) (Fββ² (fβ² β°.ββ² gβ²)) (Fββ² fβ² β±.ββ² Fββ² gβ²) ββ² = Fββ² ββ² = Fββ²
Note that, if and are fibred categories over their bases (rather than just displayed categories), then the appropriate notion of 1-cell are displayed functors that take Cartesian morphisms to Cartesian morphisms:
record Fibred-functor : Type (lvl β oβ β ββ) where field disp : Displayed-functor open Displayed-functor disp public field F-cartesian : β {a b aβ² bβ²} {f : A.Hom a b} (fβ² : β°.Hom[ f ] aβ² bβ²) β is-cartesian β° f fβ² β is-cartesian β± (F.β f) (Fββ² fβ²)