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)