module Cat.Displayed.Univalence.Thin where
open Cat.Displayed.Total public open Cat.Displayed.Base public open Total-hom public open Precategory open Displayed open Cat.Displayed.Morphism open _β [_]_
Thinly displayed structuresπ
The HoTT Bookβs version of the structure identity principle can be seen as a very early example of displayed category theory. Their standard notion of structure corresponds exactly to a displayed category, all of whose fibres are posets. Note that this is not a category fibred in posets, since the displayed category will not necessarily be a Cartesian fibration.
Here, we restrict our attention to an important special case: Categories of structures over the category of sets (for a given universe level). Since these all have thin fibres (by assumption), we refer to them as thinly displayed structures, or thin structures for short. These are of note not only because they intersect the categorical SIP defined above with the typal SIP established in the prelude modules, but also because we can work with them very directly.
record Thin-structure {β oβ²} ββ² (S : Type β β Type oβ²) : Type (lsuc β β oβ² β lsuc ββ²) where no-eta-equality field is-hom : β {x y} β (x β y) β S x β S y β Prop ββ² id-is-hom : β {x} {s : S x} β β£ is-hom (Ξ» x β x) s s β£ β-is-hom : β {x y z} {s t u} (f : y β z) (g : x β y) β (Ξ± : β£ is-hom f t u β£) (Ξ² : β£ is-hom g s t β£) β β£ is-hom (Ξ» x β f (g x)) s u β£ id-hom-unique : β {x} {s t : S x} β β£ is-hom (Ξ» x β x) s t β£ β β£ is-hom (Ξ» x β x) t s β£ β s β‘ t open Thin-structure public module _ {β oβ² ββ²} {S : Type β β Type oβ²} (spec : Thin-structure ββ² S) where
The data above conspires to make a category displayed over . The laws are trivial since is valued in propositions.
Thin-structure-over : Displayed (Sets β) oβ² ββ² Thin-structure-over .Ob[_] x = S β£ x β£ Thin-structure-over .Hom[_] f x y = β£ spec .is-hom f x y β£ Thin-structure-over .Hom[_]-set f a b = is-propβis-set hlevel! Thin-structure-over .idβ² = spec .id-is-hom Thin-structure-over ._ββ²_ f g = spec .β-is-hom _ _ f g Thin-structure-over .idrβ² fβ² = is-propβpathp (Ξ» _ β hlevel!) _ _ Thin-structure-over .idlβ² fβ² = is-propβpathp (Ξ» _ β hlevel!) _ _ Thin-structure-over .assocβ² fβ² gβ² hβ² = is-propβpathp (Ξ» _ β hlevel!) _ _ Structured-objects : Precategory _ _ Structured-objects = β« Thin-structure-over
We recall that the -structures can be made into a preorder by setting iff. the identity morphism is an -homomorphism from to . And, if this preorder is in fact a partial order, then the total category of structures is univalent β the type of identities between -structured -objects is equivalent to the type of -homomorphic -isomorphisms.
Structured-objects-is-category : is-category Structured-objects Structured-objects-is-category = is-category-total Thin-structure-over Sets-is-category $ is-category-fibrewise _ Sets-is-category Ξ» A x y β Ξ£-prop-path (Ξ» _ _ _ β β []-path _ (spec .is-hom _ _ _ .is-tr _ _)) ( spec .id-hom-unique (x .snd .fromβ²) (x .snd .toβ²) β spec .id-hom-unique (y .snd .toβ²) (y .snd .fromβ²))
By construction, such a category of structured objects admits a faithful functor into the category of sets.
Forget-structure : Functor Structured-objects (Sets β) Forget-structure = ΟαΆ Thin-structure-over Structured-hom-path : is-faithful Forget-structure Structured-hom-path p = total-hom-path Thin-structure-over p (is-propβpathp (Ξ» _ β hlevel!) _ _) module _ {β oβ² ββ²} {S : Type β β Type oβ²} {spec : Thin-structure ββ² S} where private module So = Precategory (Structured-objects spec) module Som = Cat.Morphism (Structured-objects spec) _#_ : β {a b : So.Ob} β So.Hom a b β β a β β β b β f # x = f .Total-hom.hom x _#β_ : β {a b : So.Ob} {f g : So.Hom a b } β f β‘ g β β x β f # x β‘ g # x f #β x = happly (ap hom f) x infixl 999 _#_ Homomorphism-path : β {x y : So.Ob} {f g : So.Hom x y} β (β x β f # x β‘ g # x) β f β‘ g Homomorphism-path h = Structured-hom-path spec (funext h) Homomorphism-monic : β {x y : So.Ob} (f : So.Hom x y) β (β {x y} (p : f # x β‘ f # y) β x β‘ y) β Som.is-monic f Homomorphism-monic f wit g h p = Homomorphism-path Ξ» x β wit (ap hom p $β x) record is-equational {β oβ² ββ²} {S : Type β β Type oβ²} (spec : Thin-structure ββ² S) : Type (lsuc β β oβ² β ββ²) where field invert-id-hom : β {x} {s t : S x} β β£ spec .is-hom (Ξ» x β x) s t β£ β β£ spec .is-hom (Ξ» x β x) t s β£ private module So = Precategory (Structured-objects spec) module Som = Cat.Morphism (Structured-objects spec) β«-Path : β {a b : So.Ob} β (f : So.Hom a b) β is-equiv (f #_) β a β‘ b β«-Path {a = a} {b = b} f eqv = Ξ£-pathp (n-ua (f .hom , eqv)) $ EquivJ (Ξ» B e β β st β β£ spec .is-hom (e .fst) (a .snd) st β£ β PathP (Ξ» i β S (ua e i)) (a .snd) st) (Ξ» st pres β to-pathp (ap (Ξ» e β subst S e (a .snd)) ua-id-equiv Β·Β· transport-refl _ Β·Β· spec .id-hom-unique pres (invert-id-hom pres))) (f .hom , eqv) (b .snd) (f .preserves) open is-equational public
Full-substructure : β {β oβ²} ββ² (R S : Type β β Type oβ²) β (β X β R X βͺ S X) β Thin-structure ββ² S β Thin-structure ββ² R Full-substructure _ R S embed Sst .is-hom f x y = Sst .is-hom f (embed _ .fst x) (embed _ .fst y) Full-substructure _ R S embed Sst .id-is-hom = Sst .id-is-hom Full-substructure _ R S embed Sst .β-is-hom = Sst .β-is-hom Full-substructure _ R S embed Sst .id-hom-unique Ξ± Ξ² = has-prop-fibresβinjective (embed _ .fst) (embed _ .snd) (Sst .id-hom-unique Ξ± Ξ²)