# Unordered pairs of types

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-05-01.

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.equivalences
open import foundation-core.identity-types
open import foundation-core.torsorial-type-families

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-torsorial-equiv-unordered-pair-types :
is-torsorial (equiv-unordered-pair-types A)
is-torsorial-equiv-unordered-pair-types =
is-torsorial-Eq-structure
( is-torsorial-equiv-2-Element-Type (2-element-type-unordered-pair A))
( pair (2-element-type-unordered-pair A) id-equiv)
( is-torsorial-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-torsorial-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