open import 1Lab.Path.IdentitySystem.Strict

open import Cat.Strict
open import Cat.Skeletal
open import Cat.Univalent
open import Cat.Prelude

import Cat.Reasoning
open Cat.Reasoning using (Isomorphism; id-iso)

module Cat.Gaunt where

Gaunt (pre)categories🔗

A precategory $\mathcal{C}$ is gaunt if it is univalent and strict: its type of objects $\mathrm{Ob}(\mathcal{C})$ is a set, and identity in $\mathrm{Ob}$ is equivalent to isomorphism in $\mathcal{C}$. This is a truncation condition on the isomorphisms $a \cong b : \mathcal{C}$, 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  eqv (Σ-is-hlevel  hlevel! (λ _ → is-hlevel-is-prop ))

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 

This implies that gaunt categories are skeletal: Since there is at most one isomorphism $a \cong b$, then given $\| 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.

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 ) (hlevel )
    (λ { (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 $\mathcal{C}$ is gaunt, it suffices to show that isomorphisms of $\mathcal{C}$ are equivalent to paths. $\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 $\mathcal{C}$ 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