Structure
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.
Created on 2022-02-16.
Last modified on 2025-08-14.
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 at a universe
structure : {l1 l2 : Level} (𝒫 : UU l1 → UU l2) → UU (lsuc l1 ⊔ l2) structure {l1} 𝒫 = Σ (UU l1) 𝒫 structure-family : {l1 l2 l3 : Level} (𝒫 : UU l1 → UU l2) {A : UU l3} → (A → UU l1) → UU (l2 ⊔ l3) structure-family 𝒫 {A} B = (x : A) → 𝒫 (B x) structured-family : {l1 l2 l3 : Level} (𝒫 : UU l1 → UU l2) → UU l3 → UU (lsuc l1 ⊔ l2 ⊔ l3) structured-family 𝒫 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 = structure-family 𝒫 (fiber f) structured-map : {l1 l2 l3 : Level} (𝒫 : UU (l1 ⊔ l2) → UU l3) (A : UU l1) (B : UU l2) → UU (l1 ⊔ l2 ⊔ l3) structured-map 𝒫 A B = Σ (A → B) (structure-map 𝒫) 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))
See also
Recent changes
- 2025-08-14. Fredrik Bakke. More logic (#1387).
- 2025-08-07. Fredrik Bakke. Multivariable polynomial functors (#1446).
- 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).