Unordered n-tuples of elements in a type
module foundation.unordered-tuples where
Imports
open import elementary-number-theory.natural-numbers open import foundation.decidable-equality open import foundation.homotopies open import foundation.structure-identity-principle open import foundation-core.contractible-types open import foundation-core.dependent-pair-types open import foundation-core.equivalences open import foundation-core.functions open import foundation-core.functoriality-dependent-pair-types open import foundation-core.functoriality-function-types open import foundation-core.fundamental-theorem-of-identity-types open import foundation-core.identity-types open import foundation-core.sets open import foundation-core.universe-levels open import univalent-combinatorics.complements-isolated-points open import univalent-combinatorics.equality-finite-types open import univalent-combinatorics.finite-types open import univalent-combinatorics.standard-finite-types
Idea
An unordered n-tuple of elements of a type A consists of an n-element set X
equipped with a map X → A.
Definition
unordered-tuple : {l : Level} (n : ℕ) (A : UU l) → UU (lsuc lzero ⊔ l) unordered-tuple n A = Σ (UU-Fin lzero n) (λ X → type-UU-Fin n X → A) module _ {l : Level} (n : ℕ) {A : UU l} (t : unordered-tuple n A) where type-unordered-tuple-UU-Fin : UU-Fin lzero n type-unordered-tuple-UU-Fin = pr1 t type-unordered-tuple : UU lzero type-unordered-tuple = type-UU-Fin n type-unordered-tuple-UU-Fin has-cardinality-type-unordered-tuple : has-cardinality n type-unordered-tuple has-cardinality-type-unordered-tuple = has-cardinality-type-UU-Fin n type-unordered-tuple-UU-Fin is-set-type-unordered-tuple : is-set type-unordered-tuple is-set-type-unordered-tuple = is-set-has-cardinality n has-cardinality-type-unordered-tuple has-decidable-equality-type-unordered-tuple : has-decidable-equality type-unordered-tuple has-decidable-equality-type-unordered-tuple = has-decidable-equality-has-cardinality n has-cardinality-type-unordered-tuple element-unordered-tuple : type-unordered-tuple → A element-unordered-tuple = pr2 t
Unordered tuples away from an index
module _ {l : Level} (n : ℕ) {A : UU l} (t : unordered-tuple (succ-ℕ n) A) (i : type-unordered-tuple (succ-ℕ n) t) where type-complement-point-unordered-tuple-UU-Fin : UU-Fin lzero n type-complement-point-unordered-tuple-UU-Fin = complement-point-UU-Fin n ( pair (type-unordered-tuple-UU-Fin (succ-ℕ n) t) i) type-complement-point-unordered-tuple : UU lzero type-complement-point-unordered-tuple = type-UU-Fin n type-complement-point-unordered-tuple-UU-Fin inclusion-complement-point-unordered-tuple : type-complement-point-unordered-tuple → type-unordered-tuple (succ-ℕ n) t inclusion-complement-point-unordered-tuple = inclusion-complement-point-UU-Fin n ( pair (type-unordered-tuple-UU-Fin (succ-ℕ n) t) i) unordered-tuple-complement-point-type-unordered-tuple : unordered-tuple n A pr1 unordered-tuple-complement-point-type-unordered-tuple = complement-point-UU-Fin n ( pair (type-unordered-tuple-UU-Fin (succ-ℕ n) t) i) pr2 unordered-tuple-complement-point-type-unordered-tuple = ( element-unordered-tuple (succ-ℕ n) t) ∘ ( inclusion-complement-point-unordered-tuple)
Standard unordered tuples
standard-unordered-tuple : {l : Level} (n : ℕ) {A : UU l} (f : Fin n → A) → unordered-tuple n A pr1 (standard-unordered-tuple n f) = Fin-UU-Fin' n pr2 (standard-unordered-tuple n f) = f
Properties
Equality of unordered tuples
module _ {l : Level} (n : ℕ) {A : UU l} where Eq-unordered-tuple : unordered-tuple n A → unordered-tuple n A → UU l Eq-unordered-tuple x y = Σ ( type-unordered-tuple n x ≃ type-unordered-tuple n y) ( λ e → ( element-unordered-tuple n x) ~ ( element-unordered-tuple n y ∘ map-equiv e)) refl-Eq-unordered-tuple : (x : unordered-tuple n A) → Eq-unordered-tuple x x pr1 (refl-Eq-unordered-tuple x) = id-equiv pr2 (refl-Eq-unordered-tuple x) = refl-htpy Eq-eq-unordered-tuple : (x y : unordered-tuple n A) → x ＝ y → Eq-unordered-tuple x y Eq-eq-unordered-tuple x .x refl = refl-Eq-unordered-tuple x is-contr-total-Eq-unordered-tuple : (x : unordered-tuple n A) → is-contr (Σ (unordered-tuple n A) (Eq-unordered-tuple x)) is-contr-total-Eq-unordered-tuple x = is-contr-total-Eq-structure ( λ i f e → element-unordered-tuple n x ~ (f ∘ map-equiv e)) ( is-contr-total-equiv-UU-Fin {k = n} (type-unordered-tuple-UU-Fin n x)) ( pair (type-unordered-tuple-UU-Fin n x) id-equiv) ( is-contr-total-htpy (element-unordered-tuple n x)) is-equiv-Eq-eq-unordered-tuple : (x y : unordered-tuple n A) → is-equiv (Eq-eq-unordered-tuple x y) is-equiv-Eq-eq-unordered-tuple x = fundamental-theorem-id ( is-contr-total-Eq-unordered-tuple x) ( Eq-eq-unordered-tuple x) extensionality-unordered-tuple : (x y : unordered-tuple n A) → (x ＝ y) ≃ Eq-unordered-tuple x y pr1 (extensionality-unordered-tuple x y) = Eq-eq-unordered-tuple x y pr2 (extensionality-unordered-tuple x y) = is-equiv-Eq-eq-unordered-tuple x y eq-Eq-unordered-tuple : (x y : unordered-tuple n A) → Eq-unordered-tuple x y → x ＝ y eq-Eq-unordered-tuple x y = map-inv-is-equiv (is-equiv-Eq-eq-unordered-tuple x y) isretr-eq-Eq-unordered-tuple : (x y : unordered-tuple n A) → (eq-Eq-unordered-tuple x y ∘ Eq-eq-unordered-tuple x y) ~ id isretr-eq-Eq-unordered-tuple x y = isretr-map-inv-is-equiv (is-equiv-Eq-eq-unordered-tuple x y)
Functoriality of unordered tuples
map-unordered-tuple : {l1 l2 : Level} (n : ℕ) {A : UU l1} {B : UU l2} (f : A → B) → unordered-tuple n A → unordered-tuple n B pr1 (map-unordered-tuple n f t) = type-unordered-tuple-UU-Fin n t pr2 (map-unordered-tuple n f t) = f ∘ element-unordered-tuple n t preserves-comp-map-unordered-tuple : {l1 l2 l3 : Level} (n : ℕ) {A : UU l1} {B : UU l2} {C : UU l3} (g : B → C) (f : A → B) → map-unordered-tuple n (g ∘ f) ~ (map-unordered-tuple n g ∘ map-unordered-tuple n f) preserves-comp-map-unordered-tuple n g f p = refl preserves-id-map-unordered-tuple : {l1 : Level} (n : ℕ) {A : UU l1} → map-unordered-tuple n (id {A = A}) ~ id preserves-id-map-unordered-tuple n = refl-htpy htpy-unordered-tuple : {l1 l2 : Level} (n : ℕ) {A : UU l1} {B : UU l2} {f g : A → B} → (f ~ g) → (map-unordered-tuple n f ~ map-unordered-tuple n g) htpy-unordered-tuple n {f = f} {g = g} H t = eq-Eq-unordered-tuple n ( map-unordered-tuple n f t) ( map-unordered-tuple n g t) ( pair id-equiv (H ·r element-unordered-tuple n t)) preserves-refl-htpy-unordered-tuple : {l1 l2 : Level} (n : ℕ) {A : UU l1} {B : UU l2} (f : A → B) → htpy-unordered-tuple n (refl-htpy {f = f}) ~ refl-htpy preserves-refl-htpy-unordered-tuple n f p = isretr-eq-Eq-unordered-tuple n ( map-unordered-tuple n f p) ( map-unordered-tuple n f p) ( refl) equiv-unordered-tuple : {l1 l2 : Level} (n : ℕ) {A : UU l1} {B : UU l2} → (A ≃ B) → (unordered-tuple n A ≃ unordered-tuple n B) equiv-unordered-tuple n e = equiv-tot (λ X → equiv-postcomp (type-UU-Fin n X) e) map-equiv-unordered-tuple : {l1 l2 : Level} (n : ℕ) {A : UU l1} {B : UU l2} → (A ≃ B) → (unordered-tuple n A → unordered-tuple n B) map-equiv-unordered-tuple n e = map-equiv (equiv-unordered-tuple n e) is-equiv-map-equiv-unordered-tuple : {l1 l2 : Level} (n : ℕ) {A : UU l1} {B : UU l2} → (e : A ≃ B) → is-equiv (map-equiv-unordered-tuple n e) is-equiv-map-equiv-unordered-tuple n e = is-equiv-map-equiv (equiv-unordered-tuple n e)