Unordered pairs of types
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2022-05-01.
Last modified on 2023-09-12.
module foundation.unordered-pairs-of-types where
Imports
open import foundation.dependent-pair-types open import foundation.fundamental-theorem-of-identity-types open import foundation.structure-identity-principle open import foundation.univalence open import foundation.universe-levels open import foundation.unordered-pairs open import foundation-core.contractible-types open import foundation-core.equivalences open import foundation-core.identity-types open import univalent-combinatorics.2-element-types
Idea
An unordered pair of types is an unordered pair of elements in a universe
Definitions
Unordered pairs of types
unordered-pair-types : (l : Level) → UU (lsuc l) unordered-pair-types l = unordered-pair (UU l)
Equivalences of unordered pairs of types
equiv-unordered-pair-types : {l1 l2 : Level} → unordered-pair-types l1 → unordered-pair-types l2 → UU (l1 ⊔ l2) equiv-unordered-pair-types A B = Σ ( type-unordered-pair A ≃ type-unordered-pair B) ( λ e → (i : type-unordered-pair A) → element-unordered-pair A i ≃ element-unordered-pair B (map-equiv e i)) module _ {l1 l2 : Level} (A : unordered-pair-types l1) (B : unordered-pair-types l2) (e : equiv-unordered-pair-types A B) where equiv-type-equiv-unordered-pair-types : type-unordered-pair A ≃ type-unordered-pair B equiv-type-equiv-unordered-pair-types = pr1 e map-equiv-type-equiv-unordered-pair-types : type-unordered-pair A → type-unordered-pair B map-equiv-type-equiv-unordered-pair-types = map-equiv equiv-type-equiv-unordered-pair-types equiv-element-equiv-unordered-pair-types : (i : type-unordered-pair A) → ( element-unordered-pair A i) ≃ ( element-unordered-pair B (map-equiv-type-equiv-unordered-pair-types i)) equiv-element-equiv-unordered-pair-types = pr2 e
Properties
Extensionality of unordered pairs of types
module _ {l : Level} (A : unordered-pair-types l) where id-equiv-unordered-pair-types : equiv-unordered-pair-types A A pr1 id-equiv-unordered-pair-types = id-equiv pr2 id-equiv-unordered-pair-types i = id-equiv equiv-eq-unordered-pair-types : (B : unordered-pair-types l) → A = B → equiv-unordered-pair-types A B equiv-eq-unordered-pair-types .A refl = id-equiv-unordered-pair-types is-contr-total-equiv-unordered-pair-types : is-contr (Σ (unordered-pair-types l) (equiv-unordered-pair-types A)) is-contr-total-equiv-unordered-pair-types = is-contr-total-Eq-structure ( λ I B e → (i : type-unordered-pair A) → element-unordered-pair A i ≃ B (map-equiv e i)) ( is-contr-total-equiv-2-Element-Type (2-element-type-unordered-pair A)) ( pair (2-element-type-unordered-pair A) id-equiv) ( is-contr-total-equiv-fam (element-unordered-pair A)) is-equiv-equiv-eq-unordered-pair-types : (B : unordered-pair-types l) → is-equiv (equiv-eq-unordered-pair-types B) is-equiv-equiv-eq-unordered-pair-types = fundamental-theorem-id is-contr-total-equiv-unordered-pair-types equiv-eq-unordered-pair-types extensionality-unordered-pair-types : (B : unordered-pair-types l) → (A = B) ≃ equiv-unordered-pair-types A B pr1 (extensionality-unordered-pair-types B) = equiv-eq-unordered-pair-types B pr2 (extensionality-unordered-pair-types B) = is-equiv-equiv-eq-unordered-pair-types B
Recent changes
- 2023-09-12. Egbert Rijke. Beyond foundation (#751).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).