module Cat.Displayed.Path where open Precategory open Displayed
Paths of displayed categoriesπ
If you have a pair of displayed categories and over a line of precategories , it might be interesting β if you, like me, are a lunatic β to know when they can be connected by a PathP over . This module answers that! A path between displayed categories, over a path of their corresponding bases, is a displayed functor
which is componentwise an equivalence.
private module _ {o β oβ² ββ²} {B : I β Precategory o β} {E : Displayed (B i0) oβ² ββ²} {F : Displayed (B i1) oβ² ββ²} where private module E = Displayed E module F = Displayed F
The first stepπ
We write this proof in two steps: First, we write a helper function which abstracts over the contentful part of the path (the displayed object spaces, displayed Hom spaces, etc) and automatically fills in the proofs that the laws are preserved. We have a record displayed-pathp-data which contains paths for all the interesting components:
record displayed-pathp-data : Type (lsuc (o β β β oβ² β ββ²)) where no-eta-equality field obp : PathP (Ξ» i β B i .Ob β Type oβ²) E.Ob[_] F.Ob[_] homp : PathP (Ξ» i β {x y : B i .Ob} (f : B i .Hom x y) β obp i x β obp i y β Type ββ²) E.Hom[_] F.Hom[_]
The types get increasingly unhinged as we go: The identification between displayed object spaces lies over the identification of objects of the underlying category; The identification between displayed Hom spaces lies over a path in the base category and the path of displayed object spaces we just defined.
The paths between the identity morphisms and composite morphisms lie over both of those, and they have to quantify over every implicit argument inside the path! Thatβs why this record is in a private helper module, you see.
idp : PathP (Ξ» i β β {x} {xβ² : obp i x} β homp i (B i .id) xβ² xβ²) E.idβ² F.idβ² compp : PathP (Ξ» i β β {x y z} {f : B i .Hom y z} {g : B i .Hom x y} β β {xβ² yβ² zβ²} (fβ² : homp i f yβ² zβ²) (gβ² : homp i g xβ² yβ²) β homp i (B i ._β_ f g) xβ² zβ²) E._ββ²_ F._ββ²_
An instance of this record determines a path of displayed categories,
displayed-pathp-worker : displayed-pathp-data β PathP (Ξ» i β Displayed (B i) oβ² ββ²) E F displayed-pathp-worker input = go where open displayed-pathp-data input
such that all the interesting components are literal, and the coherence components are, by definition, unimportant.
homp-set : PathP (Ξ» i β (a b : B i .Ob) (f : B i .Hom a b) (x : obp i a) (y : obp i b) β is-set (homp i f x y)) (Ξ» a b β E .Hom[_]-set) Ξ» a b β F .Hom[_]-set homp-set i a b f x y = is-propβpathp (Ξ» i β Ξ -is-hlevelΒ³ {A = B i .Ob} {B = Ξ» _ β B i .Ob} {C = Ξ» a b β B i .Hom a b} 1 Ξ» a b f β Ξ -is-hlevelΒ² {A = obp i a} {B = Ξ» _ β obp i b} 1 Ξ» x y β is-hlevel-is-prop {A = homp i f x y} 2) (Ξ» _ _ β E .Hom[_]-set) (Ξ» _ _ β F .Hom[_]-set) i a b f x y
go : PathP (Ξ» i β Displayed (B i) oβ² ββ²) E F Ob[ go i ] x = obp i x Hom[ go i ] = homp i Hom[ go i ]-set {a} {b} f x y = homp-set i a b f x y go i .idβ² = idp i go i ._ββ²_ = compp i
go i .idrβ² {a} {b} {x} {y} {f} fβ² j = is-setβsquarep (Ξ» i j β Ξ -is-hlevelΒ³ {A = B i .Ob} {B = Ξ» _ β B i .Ob} {C = Ξ» a _ β obp i a} 2 Ξ» a b x β Ξ -is-hlevelΒ³ {A = obp i b} {B = Ξ» _ β B i .Hom a b} {C = Ξ» y f β homp i f x y} 2 Ξ» y f fβ² β homp-set i a b (B i .idr f j) x y) (Ξ» i a b x y f fβ² β compp i fβ² (idp i)) (Ξ» i a b x y f fβ² β E .idrβ² fβ² i) (Ξ» i a b x y f fβ² β F .idrβ² fβ² i) (Ξ» i a b x y f fβ² β fβ²) i j a b x y f fβ² go i .idlβ² {a} {b} {x} {y} {f} fβ² j = is-setβsquarep (Ξ» i j β Ξ -is-hlevelΒ³ {A = B i .Ob} {B = Ξ» _ β B i .Ob} {C = Ξ» a _ β obp i a} 2 Ξ» a b x β Ξ -is-hlevelΒ³ {A = obp i b} {B = Ξ» _ β B i .Hom a b} {C = Ξ» y f β homp i f x y} 2 Ξ» y f fβ² β homp-set i a b (B i .idl f j) x y) (Ξ» i a b x y f fβ² β compp i (idp i) fβ²) (Ξ» i a b x y f fβ² β E .idlβ² fβ² i) (Ξ» i a b x y f fβ² β F .idlβ² fβ² i) (Ξ» i a b x y f fβ² β fβ²) i j a b x y f fβ² go i .assocβ² {a} {b} {c} {d} {w} {x} {y} {z} {f} {g} {h} fβ² gβ² hβ² j = is-setβsquarep (Ξ» i j β Ξ -is-hlevelΒ³ {A = B i .Ob} {B = Ξ» _ β B i .Ob} {C = Ξ» _ _ β B i .Ob} 2 Ξ» a b c β Ξ -is-hlevelΒ³ {A = B i .Ob} {B = Ξ» _ β obp i a} {C = Ξ» _ _ β obp i b} 2 Ξ» d w x β Ξ -is-hlevelΒ³ {A = obp i c} {B = Ξ» _ β obp i d} {C = Ξ» _ - β B i .Hom c d} 2 Ξ» y z f β Ξ -is-hlevelΒ³ {A = B i .Hom b c} {B = Ξ» _ β B i .Hom a b} {C = Ξ» _ _ β homp i f y z} 2 Ξ» g h fβ² β Ξ -is-hlevelΒ² {A = homp i g x y} {B = Ξ» _ β homp i h w x} 2 Ξ» gβ² hβ² β homp-set i a d (B i .assoc f g h j) w z) (Ξ» i a b c d w x y z f g h fβ² gβ² hβ² β compp i fβ² (compp i gβ² hβ²)) (Ξ» i a b c d w x y z f g h fβ² gβ² hβ² β E .assocβ² fβ² gβ² hβ² i) (Ξ» i a b c d w x y z f g h fβ² gβ² hβ² β F .assocβ² fβ² gβ² hβ² i) (Ξ» i a b c d w x y z f g h fβ² gβ² hβ² β compp i (compp i fβ² gβ²) hβ²) i j a b c d w x y z f g h fβ² gβ² hβ²
Complicating itπ
Suppose that we have and , together with a functor which is an isomorphism of precategories, and a functor over . This is the situation in the introduction, but where the line comes from the identity system on precategories given by isomorphisms of precategories.
module _ {o β oβ² ββ²} {B C : Precategory o β} (F : Functor B C) {β° : Displayed B oβ² ββ²} {β± : Displayed C oβ² ββ²} (G : Displayed-functor β° β± F) where private module β° = Displayed β° module β± = Displayed β± module G = Displayed-functor G module C = Precategory C module F = Functor F
The functor must be componentwise an isomorphism of types: This is the displayed equivalent of an isomorphism of precategories.
Displayed-pathp : (eqv : is-precat-iso F) β (β a β is-equiv {A = β°.Ob[ a ]} G.Fββ²) β ( β {a b} {f} {aβ² : β°.Ob[ a ]} {bβ² : β°.Ob[ b ]} β is-equiv {A = β°.Hom[ f ] aβ² bβ²} G.Fββ²) β PathP (Ξ» i β Displayed (Precategory-path F eqv i) oβ² ββ²) β° β± Displayed-pathp eqv obeqv homeqv = displayed-pathp-worker input where ps = Precategory-path F eqv
Weβll define a displayed-pathp-data. We define the paths between displayed object spaces and displayed path spaces by gluing against the ungluing of the paths in the underlying category, in the right endpoint category . Diagramatically, this looks something like
p1 : PathP (Ξ» i β ps i .Ob β Type oβ²) β°.Ob[_] β±.Ob[_] p1 i x = Glue β±.Ob[ unglue (β i) x ] Ξ» where (i = i0) β β°.Ob[ x ] , G.Fββ² , obeqv x (i = i1) β β±.Ob[ x ] , _ , id-equiv
We glue the type along β the action of the displayed functor on objects β against the line of types given by applying the space of displayed objects of to the ungluing of , giving a line of type families p1 ranging from . The situation for Hom spaces is analogous.
sys : β i (x y : ps i .Ob) (f : ps i .Hom x y) (xβ² : p1 i x) (yβ² : p1 i y) β Partial (i β¨ ~ i) _ sys i x y f xβ² yβ² (i = i0) = β°.Hom[ f ] xβ² yβ² , G.Fββ² , homeqv sys i x y f xβ² yβ² (i = i1) = β±.Hom[ f ] xβ² yβ² , _ , id-equiv p2 : PathP (Ξ» i β {x y : ps i .Ob} (f : ps i .Hom x y) β p1 i x β p1 i y β Type ββ²) β°.Hom[_] β±.Hom[_] p2 i {x} {y} f xβ² yβ² = Glue (β±.Hom[ unglue (β i) f ] (unglue (β i) xβ²) (unglue (β i) yβ²)) (sys i x y f xβ² yβ²) open displayed-pathp-data input : displayed-pathp-data input .obp = p1 input .homp = p2
We now βjustβ have to produce inhabitants of p2 along which restrict to and βs identity morphisms (and composition morphisms) at the endoints of . We can do so by gluing, now at the level of terms, against a heterogeneous composition. The details are quite nasty, but the core of it is extending the witness that respects identity to a path, over line given by gluing and ungluing the domain/codomain, between the identity maps in and .
input .idp i {x} {xβ²} = glue-inc (β i) {Tf = sys i x x (ps i .id {x}) xβ² xβ²} (Ξ» { (i = i0) β β°.idβ² ; (i = i1) β β±.idβ² }) (inS (comp (Ξ» j β β±.Hom[ p (~ j) ] (unglue (β i) xβ²) (unglue (β i) xβ²)) (β i) Ξ» { j (j = i0) β β±.idβ² ; j (i = i0) β G.F-idβ² (~ j) ; j (i = i1) β β±.idβ² })) where p : unglue (β i) (ps i .id {x}) β‘ C.id p j = hfill (β i) (~ j) Ξ» where k (k = i0) β C.id k (i = i0) β F.F-id (~ k) k (i = i1) β C.id
The case for compositions is analogous and yet much nastier, so I wonβt comment on it. You canβt make me.
input .compp i {x} {y} {z} {f} {g} {xβ²} {yβ²} {zβ²} fβ² gβ² = glue-inc (β i) {Tf = sys i x z (ps i ._β_ {x} {y} {z} f g) xβ² zβ²} (Ξ» { (i = i0) β fβ² β°.ββ² gβ² ; (i = i1) β fβ² β±.ββ² gβ² }) (inS (comp (Ξ» j β β±.Hom[ p j ] (unglue (β i) xβ²) (unglue (β i) zβ²)) (β i) Ξ» { k (k = i0) β unglue (β i) {T = Ξ» .βi=i1 β sys i y z f yβ² zβ² βi=i1 .fst} fβ² β±.ββ² unglue (β i) gβ² ; k (i = i0) β G.F-ββ² {fβ² = fβ²} {gβ² = gβ²} (~ k) ; k (i = i1) β fβ² β±.ββ² gβ² })) where p : I β C .Hom (unglue (i β¨ ~ i) x) (unglue (i β¨ ~ i) z) p j = hfill (β i) j Ξ» where k (i = i0) β F.F-β f g (~ k) k (i = i1) β f C.β g k (k = i0) β unglue (β i) f C.β unglue (β i) g
module _ {o β oβ² ββ²} {B : Precategory o β} {β° β± : Displayed B oβ² ββ²} (F : Displayed-functor β° β± Id) where private module F = Displayed-functor F module β° = Displayed β°
As one last step, we show that if the functor is displayed over the identity, the path is an actual identity, rather than a PathP.
Displayed-path : (Fβ-eqv : β a β is-equiv F.ββ²) β (Fβ-eqv : β {a b} {f : B .Hom a b} {aβ² : β°.Ob[ a ]} {bβ² : β°.Ob[ b ]} β is-equiv (F.ββ² {f = f} {aβ² = aβ²} {bβ² = bβ²})) β β° β‘ β± Displayed-path Fβ-eqv Fβ-eqv = transport (Ξ» i β PathP (Ξ» j β Displayed (to-path-refl {a = B} Precategory-identity-system i j) oβ² ββ²) β° β±) (Displayed-pathp Id F (iso id-equiv id-equiv) Fβ-eqv Fβ-eqv)