module Cat.Displayed.Univalence.Thin where

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 can be made into a preorder by setting iff. the identity morphism is an 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 is equivalent to the type of

  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)

  Extensional-Hom
    : βˆ€ {a b β„“r} ⦃ sa : Extensional (⌞ a ⌟ β†’ ⌞ b ⌟) β„“r ⦄
    β†’ Extensional (So.Hom a b) β„“r
  Extensional-Hom ⦃ sa ⦄ = injectionβ†’extensional!
    (Structured-hom-path spec) sa

  instance
    extensionality-hom : βˆ€ {a b} β†’ Extensionality (So.Hom a b)
    extensionality-hom = record { lemma = quote Extensional-Hom }

    Funlike-Hom : βˆ€ {x y} β†’ Funlike (So.Hom x y) ⌞ x ⌟ Ξ» _ β†’ ⌞ y ⌟
    Funlike-Hom = record
      { _#_ = Total-hom.hom
      }

  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)

  equiv-hom→inverse-hom
    : βˆ€ {a b : So.Ob}
    β†’ (f : ⌞ a ⌟ ≃ ⌞ b ⌟)
    β†’ ∣ spec .is-hom (Equiv.to f) (a .snd) (b .snd) ∣
    β†’ ∣ spec .is-hom (Equiv.from f) (b .snd) (a .snd) ∣
  equiv-hom→inverse-hom {a = a} {b = b} f e =
    EquivJ (Ξ» B e β†’ βˆ€ st β†’ ∣ spec .is-hom (e .fst) (a .snd) st ∣ β†’ ∣ spec .is-hom (Equiv.from e) st (a .snd) ∣)
      (Ξ» _ β†’ invert-id-hom) f (b .snd) e

  ∫-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