module Cat.Gaunt where
Gaunt (pre)categoriesπ
A precategory is gaunt if it is univalent and strict: its type of objects is a set, and identity in is equivalent to isomorphism in . This is a truncation condition on the isomorphisms , which must all be trivial.
record is-gaunt {o β} (C : Precategory o β) : Type (o β β) where field has-category : is-category C has-strict : is-strict C open Univalent.pathβiso has-category hiding (hlevel) public open StrictIds has-category has-strict renaming (K to K-iso) public
private unquoteDecl eqv = declare-record-iso eqv (quote is-gaunt) is-gaunt-is-prop : β {o β} {C : Precategory o β} β is-prop (is-gaunt C) is-gaunt-is-prop = Isoβis-hlevel 1 eqv (Ξ£-is-hlevel 1 hlevel! (Ξ» _ β is-hlevel-is-prop 2)) instance H-Level-is-gaunt : β {o β} {C : Precategory o β} {n} β H-Level (is-gaunt C) (suc n) H-Level-is-gaunt = prop-instance is-gaunt-is-prop
As one would expect, being gaunt is property of a category.
module _ {o β} {C : Precategory o β} (gaunt : is-gaunt C) where open is-gaunt gaunt open Cat.Reasoning C iso-is-prop : β {x y} β is-prop (x β y) iso-is-prop = hlevel 1
This implies that gaunt categories are skeletal: Since there is at most one isomorphism , then given , we can apply unique choice to retrieve the underlying map.
gauntβskeletal : is-skeletal C gauntβskeletal = set-identity-system (Ξ» _ _ β squash) $ β₯-β₯-rec (has-strict _ _) (has-category .to-path)
Furthermore, if a category is skeletal and univalent, it is gaunt.
skeletal+categoryβgaunt : β {o β} {C : Precategory o β} β is-skeletal C β is-category C β is-gaunt C skeletal+categoryβgaunt skel cat .is-gaunt.has-category = cat skeletal+categoryβgaunt skel cat .is-gaunt.has-strict = skeletalβstrict _ skel
This implies that gaunt categories are precisely the skeletal univalent categories.
skeletal-categoryβgaunt : β {o β} {C : Precategory o β} β (is-skeletal C Γ is-category C) β is-gaunt C skeletal-categoryβgaunt = prop-ext (hlevel 1) (hlevel 1) (Ξ» { (skel , cat) β skeletal+categoryβgaunt skel cat }) (Ξ» gaunt β gauntβskeletal gaunt , has-category gaunt) where open is-gaunt
If a category is skeletal and has only trivial automorphisms, then it is gaunt.
skeletal+trivial-automorphismsβgaunt : β {o β} {C : Precategory o β} β is-skeletal C β (β {x} β (f : Isomorphism C x x) β f β‘ id-iso C) β is-gaunt C
To show that is gaunt, it suffices to show that isomorphisms of are equivalent to paths. is skeletal, so it is straightforward to construct an inverse to pathβiso by applying to-path to the truncation of an isomorphism. Showing that this is a right inverse is straightforward, as is strict.
skeletal+trivial-automorphismsβgaunt {C = C} skel trivial-aut = skeletal+categoryβgaunt skel $ equiv-pathβidentity-system (IsoβEquiv path-iso) (Ξ» _ β transport-refl _) where open is-gaunt path-iso : β {x y} β Iso (Isomorphism C x y) (x β‘ y) path-iso .fst f = skel .to-path (inc f) path-iso .snd .is-iso.inv f = pathβiso f path-iso .snd .is-iso.rinv _ = skeletalβstrict C skel _ _ _ _
To see that this is a left inverse, we can use the fact that truncated isomorphisms form an identity system to contract the iso down into an automorphism. However, all automorphisms are trivial, which allows us to finish off the proof.
path-iso {x = x} .snd .is-iso.linv f = IdsJ skel (Ξ» y' β₯fβ₯ β β (f : Isomorphism C x y') β pathβiso (skel .to-path β₯fβ₯) β‘ f) (Ξ» f β trivial-aut _ β sym (trivial-aut _)) (inc f) f