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.
module _ {o β oβ² ββ² oβ ββ oββ² βββ²} {A : Precategory o β} {B : Precategory oβ ββ} (β° : Displayed A oβ² ββ²) (β± : Displayed B oββ² βββ²) (F : Functor A B) where private module F = Functor F module A = CR A module B = CR B module β° = Displayed β° module β± = Displayed β± lvl : Level lvl = o β oβ² β oββ² β β β ββ² β βββ²
record Displayed-functor : Type lvl where no-eta-equality 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:
module _ {o β oβ² ββ² oβ ββ oββ² βββ²} {A : Precategory o β} {B : Precategory oβ ββ} {β° : Displayed A oβ² ββ²} {β± : Displayed B oββ² βββ²} {F : Functor A B} where private module F = Functor F module A = CR A module B = CR B module β° = Displayed β° module β± = Displayed β± lvl : Level lvl = o β oβ² β oββ² β β β ββ² β βββ²
is-fibred-functor : Displayed-functor β° β± F β Type _ is-fibred-functor Fβ² = β {a b aβ² bβ²} {f : A.Hom a b} (fβ² : β°.Hom[ f ] aβ² bβ²) β is-cartesian β° f fβ² β is-cartesian β± (F.β f) (Fββ² fβ²) where open Displayed-functor Fβ²
module _ {o β oβ² ββ² oβ ββ oββ² βββ²} {A : Precategory o β} {B : Precategory oβ ββ} (β° : Displayed A oβ² ββ²) (β± : Displayed B oββ² βββ²) (F : Functor A B) where private module F = Functor F module A = CR A module B = CR B module β° = Displayed β° module β± = Displayed β± lvl : Level lvl = o β oβ² β oββ² β β β ββ² β βββ²
record Fibred-functor : Type (lvl β oβ β ββ) where no-eta-equality field disp : Displayed-functor β° β± F F-cartesian : is-fibred-functor disp open Displayed-functor disp public
One can also define the composition of displayed functors, which lies over the composition of the underlying functors.
module _ {oa βa ob βb oc βc oe βe of βf oh βh} {A : Precategory oa βa} {B : Precategory ob βb} {C : Precategory oc βc} {β° : Displayed A oe βe} {β± : Displayed B of βf} {β : Displayed C oh βh} {F : Functor B C} {G : Functor A B} where private module A = Precategory A module B = Precategory B module β° = Displayed β° module β± = Displayed β± module β = Displayed β module F = Functor F module G = Functor G open DR β open Displayed-functor infixr 30 _Fββ²_
_Fββ²_ : Displayed-functor β± β F β Displayed-functor β° β± G β Displayed-functor β° β (F Fβ G) (Fβ² Fββ² Gβ²) .Fββ² x = Fβ² .Fββ² (Gβ² .Fββ² x) (Fβ² Fββ² Gβ²) .Fββ² f = Fβ² .Fββ² (Gβ² .Fββ² f) (Fβ² Fββ² Gβ²) .F-idβ² = to-pathp $ hom[] (Fβ² .Fββ² (Gβ² .Fββ² β°.idβ²)) β‘β¨ reindex _ _ β sym (hom[]-β (ap F.Fβ G.F-id) F.F-id) β©β‘ hom[] (hom[] (Fβ² .Fββ² (Gβ² .Fββ² β°.idβ²))) β‘β¨ ap hom[] (shiftl _ Ξ» i β Fβ² .Fββ² (Gβ² .F-idβ² i)) β©β‘ hom[] (Fβ² .Fββ² β±.idβ²) β‘β¨ from-pathp (Fβ² .F-idβ²) β©β‘ β.idβ² β (Fβ² Fββ² Gβ²) .F-ββ² {f = f} {g = g} {fβ² = fβ²} {gβ² = gβ²} = to-pathp $ hom[] (Fβ² .Fββ² (Gβ² .Fββ² (fβ² β°.ββ² gβ²))) β‘β¨ reindex _ _ β sym (hom[]-β (ap F.Fβ (G.F-β f g)) (F.F-β (G.β f) (G.β g))) β©β‘ hom[] (hom[] (Fβ² .Fββ² (Gβ² .Fββ² (fβ² β°.ββ² gβ²)))) β‘β¨ ap hom[] (shiftl _ Ξ» i β Fβ² .Fββ² (Gβ² .F-ββ² {fβ² = fβ²} {gβ² = gβ²} i)) β©β‘ hom[] (Fβ² .Fββ² ((Gβ² .Fββ² fβ²) β±.ββ² (Gβ² .Fββ² gβ²))) β‘β¨ from-pathp (Fβ² .F-ββ²) β©β‘ Fβ² .Fββ² (Gβ² .Fββ² fβ²) β.ββ² Fβ² .Fββ² (Gβ² .Fββ² gβ²) β
Furthermore, there is a displayed identity functor that lies over the identity functor.
module _ {ob βb oe βe} {B : Precategory ob βb} {β° : Displayed B oe βe} where open Displayed-functor
Idβ² : Displayed-functor β° β° Id Idβ² .Fββ² x = x Idβ² .Fββ² f = f Idβ² .F-idβ² = refl Idβ² .F-ββ² = refl
The identity functor is obviously fibred.
Idβ²-fibred : is-fibred-functor Idβ² Idβ²-fibred f cart = cart Idfβ² : Fibred-functor β° β° Id Idfβ² .Fibred-functor.disp = Idβ² Idfβ² .Fibred-functor.F-cartesian = Idβ²-fibred
Vertical Functorsπ
Functors displayed over the identity functor are of particular interest. Such functors are known as vertical functors, and are commonly used to define fibrewise structure. However, they are somewhat difficult to work with if we define them directly as such, as the composite of two identity functors is not definitionally equal to the identity functor! To avoid this problem, we provide the following specialized definition.
module _ {o β oβ² ββ² oβ²β² ββ²β²} {B : Precategory o β} (β° : Displayed B oβ² ββ²) (β± : Displayed B oβ²β² ββ²β²) where private module B = Precategory B module β° = Displayed β° module β± = Displayed β± record Vertical-functor : Type (o β β β oβ² β ββ² β oβ²β² β ββ²β²) where no-eta-equality field Fββ² : β {x} (o : β°.Ob[ x ]) β β±.Ob[ x ] Fββ² : β {a b} {f : B.Hom a b} {aβ² bβ²} β β°.Hom[ f ] aβ² bβ² β β±.Hom[ f ] (Fββ² aβ²) (Fββ² bβ²) F-idβ² : β {x} {o : β°.Ob[ x ]} β PathP ( Ξ» _ β β±.Hom[ B.id ] (Fββ² o) (Fββ² o)) (Fββ² β°.idβ²) β±.idβ² F-ββ² : β {a b c} {f : B.Hom b c} {g : B.Hom a b} {aβ² bβ² cβ²} {fβ² : β°.Hom[ f ] bβ² cβ²} {gβ² : β°.Hom[ g ] aβ² bβ²} β PathP (Ξ» _ β β±.Hom[ f B.β g ] (Fββ² aβ²) (Fββ² cβ²)) (Fββ² (fβ² β°.ββ² gβ²)) (Fββ² fβ² β±.ββ² Fββ² gβ²) ββ² = Fββ² ββ² = Fββ²
This definition is equivalent to a displayed functor over the identity functor.
module _ {o β oβ² ββ² oβ²β² ββ²β²} {B : Precategory o β} {β° : Displayed B oβ² ββ²} {β± : Displayed B oβ²β² ββ²β²} where private module B = Precategory B module β° = Displayed β° module β± = Displayed β±
Displayed-functorβVertical-functor : Displayed-functor β° β± Id β Vertical-functor β° β± Displayed-functorβVertical-functor Fβ² = V where module Fβ² = Displayed-functor Fβ² open Vertical-functor V : Vertical-functor β° β± V .Fββ² = Fβ².ββ² V .Fββ² = Fβ².ββ² V .F-idβ² = Fβ².F-idβ² V .F-ββ² = Fβ².F-ββ² Vertical-functorβDisplayed-functor : Vertical-functor β° β± β Displayed-functor β° β± Id Vertical-functorβDisplayed-functor V = Fβ² where module V = Vertical-functor V open Displayed-functor Fβ² : Displayed-functor β° β± Id Fβ² .Fββ² = V.ββ² Fβ² .Fββ² = V.ββ² Fβ² .F-idβ² = V.F-idβ² Fβ² .F-ββ² = V.F-ββ²
We also provide a specialized definition for vertical fibred functors.
is-vertical-fibred : Vertical-functor β° β± β Type _ is-vertical-fibred Fβ² = β {a b aβ² bβ²} {f : B.Hom a b} (fβ² : β°.Hom[ f ] aβ² bβ²) β is-cartesian β° f fβ² β is-cartesian β± f (Fββ² fβ²) where open Vertical-functor Fβ²
open Vertical-functor Vertical-functor-path : {F G : Vertical-functor β° β±} β (p0 : β {x} β (xβ² : β°.Ob[ x ]) β F .Fββ² xβ² β‘ G .Fββ² xβ²) β (p1 : β {x y xβ² yβ²} {f : B.Hom x y} β (fβ² : β°.Hom[ f ] xβ² yβ²) β PathP (Ξ» i β β±.Hom[ f ] (p0 xβ² i) (p0 yβ² i)) (F .Fββ² fβ²) (G .Fββ² fβ²)) β F β‘ G Vertical-functor-path {F = F} {G = G} p0 p1 i .Fββ² xβ² = p0 xβ² i Vertical-functor-path {F = F} {G = G} p0 p1 i .Fββ² fβ² = p1 fβ² i Vertical-functor-path {F = F} {G = G} p0 p1 i .F-idβ² = is-propβpathp (Ξ» i β β±.Hom[ B.id ]-set _ _ (p1 β°.idβ² i) β±.idβ²) (F .F-idβ²) (G .F-idβ²) i Vertical-functor-path {F = F} {G = G} p0 p1 i .F-ββ² {fβ² = fβ²} {gβ² = gβ²} = is-propβpathp (Ξ» i β β±.Hom[ _ ]-set _ _ (p1 (fβ² β°.ββ² gβ²) i) (p1 fβ² i β±.ββ² p1 gβ² i)) (F .F-ββ² {fβ² = fβ²} {gβ² = gβ²}) (G .F-ββ² {fβ² = fβ²} {gβ² = gβ²}) i
module _ {o β oβ² ββ² oβ²β² ββ²β²} {B : Precategory o β} (β° : Displayed B oβ² ββ²) (β± : Displayed B oβ²β² ββ²β²) where private module B = Precategory B module β° = Displayed β° module β± = Displayed β± lvl : Level lvl = o β β β oβ² β ββ² β oβ²β² β ββ²β²
record Vertical-fibred-functor : Type lvl where no-eta-equality field vert : Vertical-functor β° β± F-cartesian : is-vertical-fibred vert open Vertical-functor vert public
module _ {o β oβ² ββ² oβ²β² ββ²β²} {B : Precategory o β} {β° : Displayed B oβ² ββ²} {β± : Displayed B oβ²β² ββ²β²} where private module B = Precategory B module β° = Displayed β° module β± = Displayed β±
A functor displayed over the identity functor is fibred if and only if it is a vertical fibred functor.
is-fibredβis-vertical-fibred : β (F' : Displayed-functor β° β± Id) β is-fibred-functor F' β is-vertical-fibred (Displayed-functorβVertical-functor F') is-fibredβis-vertical-fibred F' F-fib = F-fib is-vertical-fibredβis-fibred : β (F' : Vertical-functor β° β±) β is-vertical-fibred F' β is-fibred-functor (Vertical-functorβDisplayed-functor F') is-vertical-fibredβis-fibred F' F-fib = F-fib FibredβVertical-fibred : Fibred-functor β° β± Id β Vertical-fibred-functor β° β± FibredβVertical-fibred F' .Vertical-fibred-functor.vert = Displayed-functorβVertical-functor (Fibred-functor.disp F') FibredβVertical-fibred F' .Vertical-fibred-functor.F-cartesian = is-fibredβis-vertical-fibred (Fibred-functor.disp F') (Fibred-functor.F-cartesian F') Vertical-FibredβVertical : Vertical-fibred-functor β° β± β Fibred-functor β° β± Id Vertical-FibredβVertical F' .Fibred-functor.disp = Vertical-functorβDisplayed-functor (Vertical-fibred-functor.vert F') Vertical-FibredβVertical F' .Fibred-functor.F-cartesian = is-vertical-fibredβis-fibred (Vertical-fibred-functor.vert F') (Vertical-fibred-functor.F-cartesian F')
open Vertical-fibred-functor Vertical-fibred-functor-path : {F G : Vertical-fibred-functor β° β±} β (p0 : β {x} β (xβ² : β°.Ob[ x ]) β F .Fββ² xβ² β‘ G .Fββ² xβ²) β (p1 : β {x y xβ² yβ²} {f : B.Hom x y} β (fβ² : β°.Hom[ f ] xβ² yβ²) β PathP (Ξ» i β β±.Hom[ f ] (p0 xβ² i) (p0 yβ² i)) (F .Fββ² fβ²) (G .Fββ² fβ²)) β F β‘ G Vertical-fibred-functor-path {F = F} {G = G} p0 p1 i .vert = Vertical-functor-path {F = F .vert} {G = G .vert} p0 p1 i Vertical-fibred-functor-path {F = F} {G = G} p0 p1 i .F-cartesian fβ² cart = is-propβpathp (Ξ» i β is-cartesian-is-prop β± {fβ² = p1 fβ² i}) (F .F-cartesian fβ² cart) (G .F-cartesian fβ² cart) i
As promised, composition of vertical functors is much simpler.
module _ {ob βb oe βe of βf oh βh} {B : Precategory ob βb} {β° : Displayed B oe βe} {β± : Displayed B of βf} {β : Displayed B oh βh} where open Vertical-functor infixr 30 _Vβ_ infixr 30 _Vfβ_
_Vβ_ : Vertical-functor β± β β Vertical-functor β° β± β Vertical-functor β° β (Fβ² Vβ Gβ²) .Fββ² xβ² = Fβ² .Fββ² (Gβ² .Fββ² xβ²) (Fβ² Vβ Gβ²) .Fββ² fβ² = Fβ² .Fββ² (Gβ² .Fββ² fβ²) (Fβ² Vβ Gβ²) .F-idβ² = ap (Fβ² .Fββ²) (Gβ² .F-idβ²) β Fβ² .F-idβ² (Fβ² Vβ Gβ²) .F-ββ² = ap (Fβ² .Fββ²) (Gβ² .F-ββ²) β (Fβ² .F-ββ²)
Furthermore, the composite of vertical fibred functors is also fibred.
Vβ-fibred : β (Fβ² : Vertical-functor β± β) (Gβ² : Vertical-functor β° β±) β is-vertical-fibred Fβ² β is-vertical-fibred Gβ² β is-vertical-fibred (Fβ² Vβ Gβ²) Vβ-fibred Fβ² Gβ² Fβ²-fib Gβ²-fib fβ² cart = Fβ²-fib (Gβ² .Fββ² fβ²) (Gβ²-fib fβ² cart) _Vfβ_ : Vertical-fibred-functor β± β β Vertical-fibred-functor β° β± β Vertical-fibred-functor β° β (Fβ² Vfβ Gβ²) .Vertical-fibred-functor.vert = Vertical-fibred-functor.vert Fβ² Vβ Vertical-fibred-functor.vert Gβ² (Fβ² Vfβ Gβ²) .Vertical-fibred-functor.F-cartesian = Vβ-fibred (Vertical-fibred-functor.vert Fβ²) (Vertical-fibred-functor.vert Gβ²) (Vertical-fibred-functor.F-cartesian Fβ²) (Vertical-fibred-functor.F-cartesian Gβ²)
The identity functor is obviously fibred vertical.
IdV : Vertical-functor β° β° IdV = Displayed-functorβVertical-functor Idβ² IdV-fibred : is-vertical-fibred IdV IdV-fibred = is-fibredβis-vertical-fibred Idβ² Idβ²-fibred IdVf : Vertical-fibred-functor β° β° IdVf = FibredβVertical-fibred Idfβ²
Displayed Natural Transformationsπ
Just like we have defined a displayed functor lying over an ordinary functor we can define a displayed natural transformation. Assume are displayed functors over resp. and we have a natural transformation . Than one can define a displayed natural transformation lying over .
module _ {o β oβ² ββ² oβ ββ oββ² βββ²} {A : Precategory o β} {B : Precategory oβ ββ} {β° : Displayed A oβ² ββ²} {β± : Displayed B oββ² βββ²} where private module β° = Displayed β° module β± = Displayed β± open Displayed-functor open _=>_ lvl : Level lvl = o β oβ² β β β ββ² β βββ² infix 20 _=[_]=>_ record _=[_]=>_ {F : Functor A B} {G : Functor A B} (Fβ² : Displayed-functor β° β± F) (Ξ± : F => G) (Gβ² : Displayed-functor β° β± G) : Type lvl where no-eta-equality field Ξ·β² : β {x} (xβ² : β°.Ob[ x ]) β β±.Hom[ Ξ± .Ξ· x ] (Fβ² .Fββ² xβ²) (Gβ² .Fββ² xβ²) is-naturalβ² : β {x y f} (xβ² : β°.Ob[ x ]) (yβ² : β°.Ob[ y ]) (fβ² : β°.Hom[ f ] xβ² yβ²) β Ξ·β² yβ² β±.ββ² Fβ² .Fββ² fβ² β±.β‘[ Ξ± .is-natural x y f ] Gβ² .Fββ² fβ² β±.ββ² Ξ·β² xβ²
Let be two vertical functors. A displayed natural transformation between and is called a vertical natural transformation if all components of the natural transformation are vertical.
module _ {ob βb oe βe of βf} {B : Precategory ob βb} {β° : Displayed B oe βe} {β± : Displayed B of βf} where private open CR B module β° = Displayed β° module β± = Displayed β± open Vertical-functor lvl : Level lvl = ob β βb β oe β βe β βf infix 20 _=>β_ infix 20 _=>fβ_
record _=>β_ (Fβ² Gβ² : Vertical-functor β° β±) : Type lvl where no-eta-equality field Ξ·β² : β {x} (xβ² : β°.Ob[ x ]) β β±.Hom[ id ] (Fβ² .Fββ² xβ²) (Gβ² .Fββ² xβ²) is-naturalβ² : β {x y f} (xβ² : β°.Ob[ x ]) (yβ² : β°.Ob[ y ]) (fβ² : β°.Hom[ f ] xβ² yβ²) β Ξ·β² yβ² β±.ββ² Fβ² .Fββ² fβ² β±.β‘[ id-comm-sym ] Gβ² .Fββ² fβ² β±.ββ² Ξ·β² xβ²
This notion of natural transformation is also the correct one for fibred vertical functors, as there is no higher structure that needs to be preserved.
_=>fβ_ : (Fβ² Gβ² : Vertical-fibred-functor β° β±) β Type _ Fβ² =>fβ Gβ² = Fβ² .vert =>β Gβ² .vert where open Vertical-fibred-functor