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 β±
module Eβ {x} = Precategory (Fibre β° x) using (_β_)
module Fβ {x} = Precategory (Fibre β± x) using (_β_)
: Level
lvl = o β o' β oβ' β β β β' β ββ' lvl
record Displayed-functor : Type lvl where
no-eta-equality
field
: β {x} (o : β°.Ob[ x ]) β β±.Ob[ F.β x ]
Fβ' : β {a b} {f : A.Hom a b} {a' b'}
Fβ' β β°.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.
: β {x} {o : β°.Ob[ x ]}
F-id' β PathP (Ξ» i β β±.Hom[ F.F-id i ] (Fβ' o) (Fβ' o))
(Fβ' β°.id') β±.id'
: β {a b c} {f : A.Hom b c} {g : A.Hom a b} {a' b' c'}
F-β' {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 β±
: Level
lvl = o β o' β oβ' β β β β' β ββ' lvl
: Displayed-functor β° β± F β Type _
is-fibred-functor =
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 β±
: Level
lvl = o β o' β oβ' β β β β' β ββ' lvl
record Fibred-functor : Type (lvl β oβ β ββ) where
no-eta-equality
field
: Displayed-functor β° β± F
disp : is-fibred-functor disp
F-cartesian
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 $
(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') β©
hom[] .id' β
β(F' Fβ' G') .F-β' {f = f} {g = g} {f' = f'} {g' = g'} = to-pathp $
(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-β') β©
hom[] .Fβ' (G' .Fβ' f') β.β' F' .Fβ' (G' .Fβ' g') β F'
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
: Displayed-functor β° β° Id
Id' .Fβ' x = x
Id' .Fβ' f = f
Id' .F-id' = refl
Id' .F-β' = refl Id'
The identity functor is obviously fibred.
: is-fibred-functor Id'
Id'-fibred = cart
Id'-fibred f cart
: Fibred-functor β° β° Id
Idf' .Fibred-functor.disp = Id'
Idf' .Fibred-functor.F-cartesian = Id'-fibred Idf'
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 β±
module F = DR β± using (hom[])
module Eβ {x} = Precategory (Fibre β° x) using (_β_)
module Fβ {x} = Precategory (Fibre β± x) using (_β_)
record Vertical-functor : Type (o β β β o' β β' β o'' β β'') where
no-eta-equality
field
: β {x} (o : β°.Ob[ x ]) β β±.Ob[ x ]
Fβ' : β {a b} {f : B.Hom a b} {a' b'}
Fβ' β β°.Hom[ f ] a' b' β β±.Hom[ f ] (Fβ' a') (Fβ' b')
: β {x} {o : β°.Ob[ x ]}
F-id' β Fβ' (β°.id' {x} {o}) β‘ β±.id'
: β {a b c} {f : B.Hom b c} {g : B.Hom a b} {a' b' c'}
F-β' {f' : β°.Hom[ f ] b' c'} {g' : β°.Hom[ g ] a' b'}
β Fβ' (f' β°.β' g') β‘ Fβ' f' β±.β' Fβ' g'
= Fβ'
β' = Fβ' β'
abstract
F-ββ: β {x} {a b c : β°.Ob[ x ]} {f : β°.Hom[ B.id ] b c} {g : β°.Hom[ B.id ] a b}
β Fβ' (f Eβ.β g) β‘ Fβ' f Fβ.β Fβ' g
{a = a} {b} {c} {f} {g} =
F-ββ let
: Fβ' (f Eβ.β g) β±.β‘[ sym (B.idl B.id) ] Fβ' (f β°.β' g)
p = Fβ' (coe0βi (Ξ» j β β°.Hom[ B.idl B.id j ] a c) (~ i) (f β°.β' g))
p i in from-pathpβ» p β ap F.hom[] 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 β° β±
= V where
Displayed-functorβVertical-functor F' module F' = Displayed-functor F'
open Vertical-functor
: Vertical-functor β° β±
V .Fβ' = F'.β'
V .Fβ' = F'.β'
V .F-id' = F'.F-id'
V .F-β' = F'.F-β'
V
Vertical-functorβDisplayed-functor: Vertical-functor β° β± β Displayed-functor β° β± Id
= F' where
Vertical-functorβDisplayed-functor V module V = Vertical-functor V
open Displayed-functor
: Displayed-functor β° β± Id
F' .Fβ' = V.β'
F' .Fβ' = V.β'
F' .F-id' = V.F-id'
F' .F-β' = V.F-β' F'
We also provide a specialized definition for vertical fibred functors.
: Vertical-functor β° β± β Type _
is-vertical-fibred =
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
{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' =
Vertical-functor-path (Ξ» i β β±.Hom[ B.id ]-set _ _ (p1 β°.id' i) β±.id')
is-propβpathp (F .F-id')
(G .F-id') i
{F = F} {G = G} p0 p1 i .F-β' {f' = f'} {g' = g'} =
Vertical-functor-path
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 β±
: Level
lvl = o β β β o' β β' β o'' β β'' lvl
record Vertical-fibred-functor : Type lvl where
no-eta-equality
field
: Vertical-functor β° β±
vert : is-vertical-fibred vert
F-cartesian 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')
= F-fib
is-fibredβis-vertical-fibred F' F-fib
is-vertical-fibredβis-fibred: β (F' : Vertical-functor β° β±)
β is-vertical-fibred F'
β is-fibred-functor (Vertical-functorβDisplayed-functor F')
= F-fib
is-vertical-fibredβis-fibred F' F-fib
FibredβVertical-fibred: Fibred-functor β° β± Id β Vertical-fibred-functor β° β±
.Vertical-fibred-functor.vert =
FibredβVertical-fibred F' (Fibred-functor.disp F')
Displayed-functorβVertical-functor .Vertical-fibred-functor.F-cartesian =
FibredβVertical-fibred F'
is-fibredβis-vertical-fibred(Fibred-functor.disp F')
(Fibred-functor.F-cartesian F')
Vertical-FibredβVertical: Vertical-fibred-functor β° β± β Fibred-functor β° β± Id
.Fibred-functor.disp =
Vertical-FibredβVertical F' (Vertical-fibred-functor.vert F')
Vertical-functorβDisplayed-functor .Fibred-functor.F-cartesian =
Vertical-FibredβVertical F'
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
{F = F} {G = G} p0 p1 i .vert =
Vertical-fibred-functor-path {F = F .vert} {G = G .vert} p0 p1 i
Vertical-functor-path {F = F} {G = G} p0 p1 i .F-cartesian f' cart =
Vertical-fibred-functor-path (Ξ» i β is-cartesian-is-prop β± {f' = p1 f' i})
is-propβpathp (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_ _β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')
= F'-fib (G' .Fβ' f') (G'-fib f' cart)
βV-fibred F' G' F'-fib G'-fib f' cart
_βVf_
: Vertical-fibred-functor β± β
β Vertical-fibred-functor β° β±
β Vertical-fibred-functor β° β
(F' βVf G') .Vertical-fibred-functor.vert =
.vert F' βV Vertical-fibred-functor.vert G'
Vertical-fibred-functor(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.
module _
{ob βb oe βe}
{B : Precategory ob βb}
{β° : Displayed B oe βe}
where
: Vertical-functor β° β°
IdV = Displayed-functorβVertical-functor Id'
IdV
: is-vertical-fibred IdV
IdV-fibred = is-fibredβis-vertical-fibred Id' Id'-fibred
IdV-fibred
: Vertical-fibred-functor β° β°
IdVf = FibredβVertical-fibred Idf' IdVf
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 _=>_
: Level
lvl = o β o' β β β β' β ββ'
lvl 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 β±
module Fβ {x} = CR (Fibre β± x)
open Vertical-functor
: Level
lvl = ob β βb β oe β βe β βf
lvl
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'
abstract
is-naturalβ: β {x} (x' y' : β°.Ob[ x ]) (f' : β°.Hom[ id ] x' y')
β Ξ·' y' Fβ.β F' .Fβ' f' β‘ G' .Fβ' f' Fβ.β Ξ·' x'
= ap hom[] (from-pathpβ» (is-natural' x y f)) β sym (duplicate _ _ _) where
is-naturalβ x y f open DR β± using (hom[] ; duplicate)
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' .vert =>β G' .vert
F' =>fβ G' where open Vertical-fibred-functor
private unquoteDecl eqv = declare-record-iso eqv (quote _=>β_)
instance
Extensional-=>β: β {βr F' G'}
β β¦ _ : Extensional (β {x} (x' : β°.Ob[ x ]) β β±.Hom[ id ] (F' .Fβ' x') (G' .Fβ' x')) βr β¦
β Extensional (F' =>β G') βr
{F' = F'} {G' = G'} β¦ e β¦ = injectionβextensional! {f = _=>β_.Ξ·'}
Extensional-=>β (Ξ» p β Iso.injective eqv (Ξ£-prop-path! p)) e
: β {F' G'} {n} β H-Level (F' =>β G') (2 + n)
H-Level-=>β = basic-instance 2 (Isoβis-hlevel 2 eqv (hlevel 2))
H-Level-=>β
open _=>β_
: β {F} β F =>β F
idntβ .Ξ·' x' = β±.id'
idntβ .is-natural' x' y' f' = to-pathp (DR.id-comm[] β±)
idntβ
_βntβ_ : β {F G H} β G =>β H β F =>β G β F =>β H
(f βntβ g) .Ξ·' x' = f .Ξ·' _ Fβ.β g .Ξ·' x'
_βntβ_ {F = F} {G = G} {H = H} f g .is-natural' {f = b} x' y' f' =
let open DR β± using (hom[] ; whisker-l ; duplicate ; pullr' ; extendl' ; unwhisker-r) in to-pathp (
(whisker-l (idl id))
ap hom[] (duplicate (ap (_β b) (idl id) β id-comm-sym) _ _)
ββ sym (from-pathpβ» (pullr' id-comm-sym (g .is-natural' _ _ _)
ββ ap hom[] {q = ap (_β b) (idl id) β id-comm-sym β introl refl}))
(duplicate (eliml refl) _ _)
ββ sym (from-pathpβ» (extendl' id-comm-sym (f .is-natural' x' y' f') {q = extendl id-comm-sym}))
ββ ap hom[] (duplicate (ap (b β_) (idl id)) (eliml refl) _)
ββ sym _ _)
ββ unwhisker-r
module _
{ob βb oc βc od βd oe βe}
{B : Precategory ob βb}
{π : Displayed B oc βc}
{π : Displayed B od βd}
{β° : Displayed B oe βe}
{F G : Vertical-functor π β°} {H K : Vertical-functor π π}
(Ξ± : F =>β G) (Ξ² : H =>β K) where
open Vertical-functor
open _=>β_
open CR B
private module E {x} = CR (Fibre β° x) using (_β_)
_ββ_ : (F βV H) =>β (G βV K)
_ββ_ .Ξ·' x' = G .Fβ' (Ξ² .Ξ·' _) E.β Ξ± .Ξ·' _
_ββ_ .is-natural' x' y' f' = to-pathp (
(whisker-l (idl id))
ap hom[] (duplicate (ap (_β _) (idl id) β id-comm-sym) _ _)
ββ sym (from-pathpβ» (pullr' _ (Ξ± .is-natural' _ _ _) {q = pullr id-comm-sym}))
ββ ap hom[] (duplicate (eliml refl) _ _)
ββ sym (from-pathpβ»
ββ ap hom[] (extendl' _ (symP (G .F-β') β[] (apd (Ξ» i β G .Fβ') (Ξ² .is-natural' _ _ _) β[] G .F-β'))
{q = extendl id-comm-sym}))
(duplicate (ap (_ β_) (idl id)) _ _) ββ unwhisker-r _ _)
ββ sym where
open DR β° using (hom[] ; whisker-l ; duplicate ; pullr' ; extendl' ; unwhisker-r)
open Displayed β° using (_β[]_)