Subuniverses
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Victor Blanchi and Eléonore Mangel.
Created on 2022-02-16.
Last modified on 2023-09-28.
module foundation.subuniverses where
Imports
open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types open import foundation.equivalences open import foundation.functoriality-dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.subtype-identity-principle open import foundation.type-arithmetic-dependent-pair-types open import foundation.univalence open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.embeddings open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.subtypes open import foundation-core.transport-along-identifications
Idea
Subuniverses are subtypes of the universe.
Definitions
Subuniverses
is-subuniverse : {l1 l2 : Level} (P : UU l1 → UU l2) → UU ((lsuc l1) ⊔ l2) is-subuniverse P = is-subtype P subuniverse : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2) subuniverse l1 l2 = subtype l2 (UU l1) is-subtype-subuniverse : {l1 l2 : Level} (P : subuniverse l1 l2) (X : UU l1) → is-prop (type-Prop (P X)) is-subtype-subuniverse P X = is-prop-type-Prop (P X) module _ {l1 l2 : Level} (P : subuniverse l1 l2) where type-subuniverse : UU ((lsuc l1) ⊔ l2) type-subuniverse = type-subtype P is-in-subuniverse : UU l1 → UU l2 is-in-subuniverse = is-in-subtype P is-prop-is-in-subuniverse : (X : UU l1) → is-prop (is-in-subuniverse X) is-prop-is-in-subuniverse = is-prop-is-in-subtype P inclusion-subuniverse : type-subuniverse → UU l1 inclusion-subuniverse = inclusion-subtype P is-in-subuniverse-inclusion-subuniverse : (X : type-subuniverse) → is-in-subuniverse (inclusion-subuniverse X) is-in-subuniverse-inclusion-subuniverse = pr2 is-emb-inclusion-subuniverse : is-emb inclusion-subuniverse is-emb-inclusion-subuniverse = is-emb-inclusion-subtype P emb-inclusion-subuniverse : type-subuniverse ↪ UU l1 emb-inclusion-subuniverse = emb-subtype P
The predicate of essentially being in a subuniverse
module _ {l1 l2 : Level} (P : subuniverse l1 l2) where is-essentially-in-subuniverse : {l3 : Level} (X : UU l3) → UU (lsuc l1 ⊔ l2 ⊔ l3) is-essentially-in-subuniverse X = Σ (type-subuniverse P) (λ Y → inclusion-subuniverse P Y ≃ X) is-prop-is-essentially-in-subuniverse : {l3 : Level} (X : UU l3) → is-prop (is-essentially-in-subuniverse X) is-prop-is-essentially-in-subuniverse X = is-prop-is-proof-irrelevant ( λ ((X' , p) , e) → is-contr-total-Eq-subtype ( is-contr-equiv' ( Σ (UU _) (λ T → T ≃ X')) ( equiv-tot (equiv-postcomp-equiv e)) ( is-contr-total-equiv' X')) ( is-prop-is-in-subuniverse P) ( X') ( e) ( p)) is-essentially-in-subuniverse-Prop : {l3 : Level} (X : UU l3) → Prop (lsuc l1 ⊔ l2 ⊔ l3) pr1 (is-essentially-in-subuniverse-Prop X) = is-essentially-in-subuniverse X pr2 (is-essentially-in-subuniverse-Prop X) = is-prop-is-essentially-in-subuniverse X
Global subuniverses
is-global-subuniverse : (α : Level → Level) (P : (l : Level) → subuniverse l (α l)) → (l1 l2 : Level) → UU (α l1 ⊔ α l2 ⊔ lsuc l1 ⊔ lsuc l2) is-global-subuniverse α P l1 l2 = (X : UU l1) (Y : UU l2) → X ≃ Y → type-Prop (P l1 X) → type-Prop (P l2 Y) record global-subuniverse (α : Level → Level) : UUω where field subuniverse-global-subuniverse : (l : Level) → subuniverse l (α l) is-global-global-subuniverse : (l1 l2 : Level) → is-global-subuniverse α subuniverse-global-subuniverse l1 l2 open global-subuniverse public module _ (α : Level → Level) (P : global-subuniverse α) where is-in-global-subuniverse : {l : Level} → UU l → UU (α l) is-in-global-subuniverse X = is-in-subuniverse (subuniverse-global-subuniverse P _) X
Properties
Subuniverses are closed under equivalences
is-in-subuniverse-equiv : {l1 l2 : Level} (P : subuniverse l1 l2) {X Y : UU l1} → X ≃ Y → is-in-subuniverse P X → is-in-subuniverse P Y is-in-subuniverse-equiv P e = tr (is-in-subuniverse P) (eq-equiv _ _ e) is-in-subuniverse-equiv' : {l1 l2 : Level} (P : subuniverse l1 l2) {X Y : UU l1} → X ≃ Y → is-in-subuniverse P Y → is-in-subuniverse P X is-in-subuniverse-equiv' P e = tr (is-in-subuniverse P) (inv (eq-equiv _ _ e))
Characterization of the identity type of subuniverses
module _ {l1 l2 : Level} (P : subuniverse l1 l2) where equiv-subuniverse : (X Y : type-subuniverse P) → UU l1 equiv-subuniverse X Y = (pr1 X) ≃ (pr1 Y) equiv-eq-subuniverse : (s t : type-subuniverse P) → s = t → equiv-subuniverse s t equiv-eq-subuniverse (pair X p) .(pair X p) refl = id-equiv abstract is-contr-total-equiv-subuniverse : (s : type-subuniverse P) → is-contr (Σ (type-subuniverse P) (λ t → equiv-subuniverse s t)) is-contr-total-equiv-subuniverse (pair X p) = is-contr-total-Eq-subtype ( is-contr-total-equiv X) ( is-subtype-subuniverse P) ( X) ( id-equiv) ( p) is-contr-total-equiv-subuniverse' : (s : type-subuniverse P) → is-contr (Σ (type-subuniverse P) (λ t → equiv-subuniverse t s)) is-contr-total-equiv-subuniverse' (pair X p) = is-contr-total-Eq-subtype ( is-contr-total-equiv' X) ( is-subtype-subuniverse P) ( X) ( id-equiv) ( p) abstract is-equiv-equiv-eq-subuniverse : (s t : type-subuniverse P) → is-equiv (equiv-eq-subuniverse s t) is-equiv-equiv-eq-subuniverse (pair X p) = fundamental-theorem-id ( is-contr-total-equiv-subuniverse (pair X p)) ( equiv-eq-subuniverse (pair X p)) extensionality-subuniverse : (s t : type-subuniverse P) → (s = t) ≃ equiv-subuniverse s t pr1 (extensionality-subuniverse s t) = equiv-eq-subuniverse s t pr2 (extensionality-subuniverse s t) = is-equiv-equiv-eq-subuniverse s t eq-equiv-subuniverse : {s t : type-subuniverse P} → equiv-subuniverse s t → s = t eq-equiv-subuniverse {s} {t} = map-inv-is-equiv (is-equiv-equiv-eq-subuniverse s t) compute-eq-equiv-id-equiv-subuniverse : {s : type-subuniverse P} → eq-equiv-subuniverse {s} {s} (id-equiv {A = pr1 s}) = refl compute-eq-equiv-id-equiv-subuniverse = is-retraction-map-inv-equiv (extensionality-subuniverse _ _) refl
Equivalences of families of types in a subuniverse
fam-subuniverse : {l1 l2 l3 : Level} (P : subuniverse l1 l2) (X : UU l3) → UU (lsuc l1 ⊔ l2 ⊔ l3) fam-subuniverse P X = X → type-subuniverse P module _ {l1 l2 l3 : Level} (P : subuniverse l1 l2) {X : UU l3} where equiv-fam-subuniverse : (Y Z : fam-subuniverse P X) → UU (l1 ⊔ l3) equiv-fam-subuniverse Y Z = (x : X) → equiv-subuniverse P (Y x) (Z x) id-equiv-fam-subuniverse : (Y : fam-subuniverse P X) → equiv-fam-subuniverse Y Y id-equiv-fam-subuniverse Y x = id-equiv is-contr-total-equiv-fam-subuniverse : (Y : fam-subuniverse P X) → is-contr (Σ (fam-subuniverse P X) (equiv-fam-subuniverse Y)) is-contr-total-equiv-fam-subuniverse Y = is-contr-total-Eq-Π ( λ x → equiv-subuniverse P (Y x)) ( λ x → is-contr-total-equiv-subuniverse P (Y x)) equiv-eq-fam-subuniverse : (Y Z : fam-subuniverse P X) → Y = Z → equiv-fam-subuniverse Y Z equiv-eq-fam-subuniverse Y .Y refl = id-equiv-fam-subuniverse Y is-equiv-equiv-eq-fam-subuniverse : (Y Z : fam-subuniverse P X) → is-equiv (equiv-eq-fam-subuniverse Y Z) is-equiv-equiv-eq-fam-subuniverse Y = fundamental-theorem-id ( is-contr-total-equiv-fam-subuniverse Y) ( equiv-eq-fam-subuniverse Y) extensionality-fam-subuniverse : (Y Z : fam-subuniverse P X) → (Y = Z) ≃ equiv-fam-subuniverse Y Z pr1 (extensionality-fam-subuniverse Y Z) = equiv-eq-fam-subuniverse Y Z pr2 (extensionality-fam-subuniverse Y Z) = is-equiv-equiv-eq-fam-subuniverse Y Z eq-equiv-fam-subuniverse : (Y Z : fam-subuniverse P X) → equiv-fam-subuniverse Y Z → (Y = Z) eq-equiv-fam-subuniverse Y Z = map-inv-is-equiv (is-equiv-equiv-eq-fam-subuniverse Y Z)
See also
Recent changes
- 2023-09-28. Egbert Rijke and Fredrik Bakke. Cyclic types (#800).
- 2023-09-12. Egbert Rijke. Beyond foundation (#751).
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-06-28. Fredrik Bakke. Localizations and other things (#655).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).