{-# OPTIONS --lossy-unification #-}
open import 1Lab.Function.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 ∫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 .$ The laws are trivial since $H$ is valued in propositions.

  Thin-structure-over : Displayed (Sets ℓ) o' ℓ'
  Thin-structure-over = with-thin-display record where
    Ob[_]      x = S ∣ x ∣
    Hom[_] f x y = ∣ spec .is-hom f x y ∣

    id'      = spec .id-is-hom
    _∘'_ f g = spec .∘-is-hom _ _ f g

  Structured-objects : Precategory _ _
  Structured-objects = ∫ Thin-structure-over

We recall that the $S -structures$ can be made into a preorder by setting $α \leq β$ iff. the identity morphism is an $H -homomorphism$ 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 $S -structured$ $B -objects$ is equivalent to the type of $H -homomorphic$ $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 = ∫Hom-path Thin-structure-over p prop!

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)

  instance
    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

  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 = ext λ x → wit (ap fst 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)

  abstract
    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

  total-iso
    : ∀ {a b : So.Ob}
    → (f : ⌞ a ⌟ ≃ ⌞ b ⌟)
    → ∣ spec .is-hom (Equiv.to f) (a .snd) (b .snd) ∣
    → a Som.≅ b
  total-iso f e = Som.make-iso
    (∫hom (Equiv.to f) e)
    (∫hom (Equiv.from f) (equiv-hom→inverse-hom f e))
    (ext (Equiv.ε f))
    (ext (Equiv.η f))

  ∫-Path
    : ∀ {a b : So.Ob}
    → (f : So.Hom a b)
    → is-equiv (f ·_)
    → a ≡ b
  ∫-Path {a = a} {b = b} f eqv = Univalent.iso→path
    (Structured-objects-is-category spec)
    (total-iso ((f ·_) , eqv) (f .snd))

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 α β)