{-# OPTIONS --lossy-unification #-}
open import 1Lab.Equiv.Embedding

open import Cat.Displayed.Univalence
open import Cat.Functor.Properties
open import Cat.Displayed.Total
open import Cat.Displayed.Base
open import Cat.Instances.Sets
open import Cat.Prelude

import Cat.Displayed.Morphism
import Cat.Morphism

module Cat.Displayed.Univalence.Thin where


open Cat.Displayed.Total public
open Cat.Displayed.Base public
open Total-hom public
open Precategory
open Displayed
open Cat.Displayed.Morphism
open _β‰…[_]_

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 B\mathcal{B}. The laws are trivial since HH 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 SS-structures can be made into a preorder by setting α≀β\alpha \le \beta iff. the identity morphism is an HH-homomorphism from Ξ±\alpha to Ξ²\beta. And, if this preorder is in fact a partial order, then the total category of structures is univalent β€” the type of identities between SS-structured B\mathcal{B}-objects is equivalent to the type of HH-homomorphic B\mathcal{B}-isomorphisms.

  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)

  _#_ : βˆ€ {a b : So.Ob} β†’ So.Hom a b β†’ ⌞ a ⌟ β†’ ⌞ b ⌟
  f # x = f .Total-hom.hom x

  _#β‚š_ : βˆ€ {a b : So.Ob} {f g : So.Hom a b } β†’ f ≑ g β†’ βˆ€ x β†’ f # x ≑ g # x
  f #β‚š x = happly (ap hom f) x

  infixl 999 _#_

  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)

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

Full-substructure
  : βˆ€ {β„“ oβ€²} β„“β€² (R S : Type β„“ β†’ Type oβ€²)
  β†’ (βˆ€ X β†’ R X β†ͺ S X)
  β†’ Thin-structure β„“β€² S
  β†’ Thin-structure β„“β€² R
Full-substructure _ R S embed Sst .is-hom f x y =
  Sst .is-hom f (embed _ .fst x) (embed _ .fst y)
Full-substructure _ R S embed Sst .id-is-hom = Sst .id-is-hom
Full-substructure _ R S embed Sst .∘-is-hom = Sst .∘-is-hom
Full-substructure _ R S embed Sst .id-hom-unique Ξ± Ξ² =
  has-prop-fibres→injective (embed _ .fst) (embed _ .snd)
    (Sst .id-hom-unique Ξ± Ξ²)