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 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 = hlevel 2 Thin-structure-over .id' = spec .id-is-hom Thin-structure-over ._∘'_ f g = spec .∘-is-hom _ _ f g Thin-structure-over .idr' f' = prop! Thin-structure-over .idl' f' = prop! Thin-structure-over .assoc' f' g' h' = prop! 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 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 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) 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 (total-hom (Equiv.to f) e) (total-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 .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 α β)