open import Cat.Displayed.Base open import Cat.Prelude import Cat.Reasoning as CR import Cat.Displayed.Morphism as DM module Cat.Displayed.Total {o β oβ² ββ²} {B : Precategory o β} (E : Displayed B oβ² ββ²) where open Displayed E open DM E open CR B
The Total Category of a Displayed Categoryπ
So far, weβve been thinking of displayed categories as βcategories of structuresβ over some base category. However, itβs often useful to consider a more βbundled upβ notion of structure, where the carrier and the structure are considered as a singular object. For instance, if we consider the case of algebraic structures, we often want to think about βa monoidβ as a singular thing, as opposed to structure imposed atop some set.
Constructing the total category does exactly this. The objects are pairs of an object from the base, an object from the displayed category that lives over it.
Note that we use a sigma type here instead of a record for technical reasons: this makes it simpler to work with algebraic structures.
Total : Type (o β oβ²) Total = Ξ£[ Carrier β Ob ] Ob[ Carrier ]
The situation is similar for morphisms: we bundle up a morphism from the base category along with a morphism that lives above it.
record Total-hom (X Y : Total) : Type (β β ββ²) where constructor total-hom field hom : Hom (X .fst) (Y .fst) preserves : Hom[ hom ] (X .snd) (Y .snd) open Total-hom
As is tradition, we need to prove some silly lemmas showing that the bundled morphisms form an hset, and another characterizing the paths between morphisms.
total-hom-is-set : β (X Y : Total) β is-set (Total-hom X Y) total-hom-is-set X Y = Isoβis-hlevel 2 eqv $ Ξ£-is-hlevel 2 (hlevel 2) (Ξ» a β Hom[ _ ]-set _ _) total-hom-path : β {X Y : Total} {f g : Total-hom X Y} β (p : f .hom β‘ g .hom) β f .preserves β‘[ p ] g .preserves β f β‘ g total-hom-path p pβ² i .hom = p i total-hom-path {f = f} {g = g} p pβ² i .preserves = pβ² i
With all that in place, we can construct the total category!
β« : Precategory (o β oβ²) (β β ββ²) β« .Precategory.Ob = Total β« .Precategory.Hom = Total-hom β« .Precategory.Hom-set = total-hom-is-set β« .Precategory.id = total-hom id idβ² β« .Precategory._β_ f g = total-hom (f .hom β g .hom) (f .preserves ββ² g .preserves) β« .Precategory.idr _ = total-hom-path (idr _) (idrβ² _) β« .Precategory.idl _ = total-hom-path (idl _) (idlβ² _) β« .Precategory.assoc _ _ _ = total-hom-path (assoc _ _ _) (assocβ² _ _ _)
Morphisms in the total categoryπ
Isomorphisms in the total category of consist of pairs of isomorphisms in and .
private module β«E = CR β« total-isoβiso : β {x y} β x β«E.β y β x .fst β y .fst total-isoβiso f = make-iso (β«E._β _.to f .hom) (β«E._β _.from f .hom) (ap hom $ β«E._β _.invl f) (ap hom $ β«E._β _.invr f) total-isoβiso[] : β {x y} β (f : x β«E.β y) β x .snd β [ total-isoβiso f ] y .snd total-isoβiso[] f = make-iso[ total-isoβiso f ] (β«E._β _.to f .preserves) (β«E._β _.from f .preserves) (ap preserves $ β«E._β _.invl f) (ap preserves $ β«E._β _.invr f)