module Cat.Gaunt where

Gaunt (pre)categoriesπŸ”—

A precategory C\mathcal{C} is gaunt if it is univalent and strict: its type of objects Ob(C)\mathrm{Ob}(\mathcal{C}) is a set, and identity in Ob\mathrm{Ob} is equivalent to isomorphism in C\mathcal{C}. This is a truncation condition on the isomorphisms a≅b:Ca \cong b : \mathcal{C}, which must all be trivial.

record is-gaunt {o β„“} (C : Precategory o β„“) : Type (o βŠ” β„“) where
    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

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 aβ‰…ba \cong b, then given βˆ₯aβ‰…bβˆ₯\| a \cong b \|, 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.

  : βˆ€ {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.

  : βˆ€ {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.

  : βˆ€ {o β„“} {C : Precategory o β„“}
  β†’ is-skeletal C
  β†’ (βˆ€ {x} β†’ (f : Isomorphism C x x) β†’ f ≑ id-iso C)
  β†’ is-gaunt C

To show that C\mathcal{C} is gaunt, it suffices to show that isomorphisms of C\mathcal{C} are equivalent to paths. C\mathcal{C} 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 C\mathcal{C} is strict.

skeletal+trivial-automorphisms→gaunt {C = C} skel trivial-aut =
  skeletal+category→gaunt skel $
      (Iso→Equiv path-iso)
      (Ξ» _ β†’ transport-refl _)
    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