Structure
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.
Created on 2022-02-16.
Last modified on 2025-02-10.
module foundation.structure where
Imports
open import foundation.dependent-pair-types open import foundation.univalence open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.fibers-of-maps open import foundation-core.identity-types open import foundation-core.transport-along-identifications
Idea
Given a type family 𝒫
on the universe, a 𝒫
-structured type¶
consists of a type A
equipped with an element of type 𝒫 A
.
Definitions
structure : {l1 l2 : Level} (𝒫 : UU l1 → UU l2) → UU (lsuc l1 ⊔ l2) structure {l1} 𝒫 = Σ (UU l1) 𝒫 fam-structure : {l1 l2 l3 : Level} (𝒫 : UU l1 → UU l2) (A : UU l3) → UU (lsuc l1 ⊔ l2 ⊔ l3) fam-structure 𝒫 A = A → structure 𝒫 structure-map : {l1 l2 l3 : Level} (𝒫 : UU (l1 ⊔ l2) → UU l3) {A : UU l1} {B : UU l2} (f : A → B) → UU (l2 ⊔ l3) structure-map 𝒫 {A} {B} f = (b : B) → 𝒫 (fiber f b) hom-structure : {l1 l2 l3 : Level} (𝒫 : UU (l1 ⊔ l2) → UU l3) → UU l1 → UU l2 → UU (l1 ⊔ l2 ⊔ l3) hom-structure 𝒫 A B = Σ (A → B) (structure-map 𝒫) structure-equality : {l1 l2 : Level} (𝒫 : UU l1 → UU l2) → UU l1 → UU (l1 ⊔ l2) structure-equality 𝒫 A = (x y : A) → 𝒫 (x = y)
Properties
Having structure is closed under equivalences
This is a consequence of the univalence axiom
has-structure-equiv : {l1 l2 : Level} (𝒫 : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → 𝒫 X → 𝒫 Y has-structure-equiv 𝒫 e = tr 𝒫 (eq-equiv e) has-structure-equiv' : {l1 l2 : Level} (𝒫 : UU l1 → UU l2) {X Y : UU l1} → X ≃ Y → 𝒫 Y → 𝒫 X has-structure-equiv' 𝒫 e = tr 𝒫 (inv (eq-equiv e))
Recent changes
- 2025-02-10. Fredrik Bakke. Some extensions of the fundamental theorem of identity types (#1243).
- 2024-01-12. Fredrik Bakke. Make type arguments implicit for
eq-equiv
(#998). - 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).