{-# OPTIONS --without-K #-}

open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.booleans
open import foundation.cartesian-product-types
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equality-cartesian-product-types
open import foundation.equality-coproduct-types
open import foundation.equivalences
open import foundation.equivalence-extensionality
open import foundation.existential-quantification
open import foundation.function-types
open import foundation.function-extensionality
open import foundation.functoriality-cartesian-product-types
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.functoriality-truncation
open import foundation.identity-types
open import foundation.negation
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.sets
open import foundation.transport-along-identifications
open import foundation.truncated-types
open import foundation.truncations
open import foundation.truncation-levels
  renaming (truncation-level-minus-one-ℕ to minus-one;
    truncation-level-minus-two-ℕ to minus-two;
    truncation-level-ℕ to to-𝕋)
open import foundation.type-arithmetic-booleans
open import foundation.type-arithmetic-cartesian-product-types
open import foundation.type-arithmetic-empty-type
open import foundation.type-arithmetic-unit-type
open import foundation.type-theoretic-principle-of-choice
open import foundation.unit-type
open import foundation.universe-levels

open import order-theory.accessible-elements-relations
open import order-theory.well-founded-orders

open import e-structure.core
open import notation as N

module e-structure.property.unordered-tupling
  {i j} (((M , _∈_) , p) : ∈-structure i j) where

[_]-UnorderedTupling : ℕ → {k : Level} → UU k → UU (i ⊔ (j ⊔ k))
[ n ]-UnorderedTupling I = (v : I → M)
  → Σ M λ ｛v｝ → (z : M) → (z ∈ ｛v｝) ≃ type-trunc (minus-one n ) (Σ I λ i → v i == z)

-- Special case
0-UnorderedTupling : ∀ {k} → UU k → UU (i ⊔ (j ⊔ k))
0-UnorderedTupling = [ zero-ℕ ]-UnorderedTupling

∞-UnorderedTupling : ∀ {k} → UU k → UU (i ⊔ (j ⊔ k))
∞-UnorderedTupling I = (v : I → M)
  → Σ M λ [v] → (z : M) → (z ∈ [v]) ≃ Σ I λ i → v i == z

open e-structure.core.extensionality ((M , _∈_) , p)
open e-structure.core.mere-sets ((M , _∈_) , p)

-- Special cases of unordered tupling

-- The empty set
EmptySet : UU (i ⊔ j)
EmptySet = Σ M (λ ∅ → (x : M) → (x ∈ ∅) ≃ empty)

module empty-set where
  module notation (empty-set : EmptySet) where

    ∅ : M
    ∅ = pr1 empty-set

  module properties (empty-set : EmptySet) where

    open notation empty-set

    mere-set-empty-set : mere-set ∅
    mere-set-empty-set x = is-prop-equiv (pr2 empty-set x) is-prop-empty

    accessible-empty-set : is-accessible-element-Relation _∈_ ∅
    accessible-empty-set = access (λ {y} y∈∅ → ex-falso (map-equiv (pr2 empty-set y) y∈∅))

-- 0-singletons
0-Singletons : UU (i ⊔ j)
0-Singletons = (x : M) →
  Σ M λ ｛x｝ → (z : M) → (z ∈ ｛x｝) ≃ type-trunc-Prop (x == z)

module 0-singletons where
  module notation (0-singletons : 0-Singletons) where

    ｛_｝ : M → M
    ｛ x ｝ = pr1 (0-singletons x)

-- n-singletons
[_]-Singletons : ℕ → UU (i ⊔ j)
[ n ]-Singletons = (x : M) →
  Σ M λ ｛x｝ → (z : M) → (z ∈ ｛x｝) ≃ type-trunc (minus-one n) (x == z)

module singletons where
  module notation {n : ℕ} (singletons : [ n ]-Singletons) where

    ｛_｝ : M → M
    ｛ x ｝ = pr1 (singletons x)

-- ∞-Singletons
∞-Singletons : UU (i ⊔ j)
∞-Singletons = (x : M) →
  Σ M λ [x] → (z : M) → (z ∈ [x]) ≃ (x == z)

module ∞-singletons where
  module notation (∞-singletons : ∞-Singletons) where

    [_] : M → M
    [ x ] = pr1 (∞-singletons x)

-- Unordered pairs of distinct elements
UnorderedPairs' : UU (i ⊔ j)
UnorderedPairs' = (x y : M) →
  Σ M λ [x,y] → ¬ (x == y) → (z : M) → (z ∈ [x,y]) ≃ ((x == z) + (y == z))

module unordered-pairs' where
  module notation (unordered-pairs' : UnorderedPairs') where

    [_,,_]' : M → M → M
    [ x ,, y ]' = pr1 (unordered-pairs' x y)

-- n-unordered pairs
[_]-UnorderedPairs : ℕ → UU (i ⊔ j)
[ n ]-UnorderedPairs = (x y : M) →
  Σ M (λ ｛x,y｝ → (z : M) → (z ∈ ｛x,y｝) ≃ type-trunc (minus-one n) ((x == z) + (y == z)))

module unordered-pairs where
  module notation {n : ℕ} (unordered-pairs : [ n ]-UnorderedPairs) where

    ｛_,,_｝ : M → M → M
    ｛ x ,, y ｝ = pr1 (unordered-pairs x y)

-- ∞-unordered pairs
∞-UnorderedPairs : UU (i ⊔ j)
∞-UnorderedPairs = (x y : M) →
  Σ M (λ [x,y] → (z : M) → (z ∈ [x,y]) ≃ ((x == z) + (y == z)))

module ∞-unordered-pairs where
  module notation (∞-unordered-pairs : ∞-UnorderedPairs) where

    [_,,_] : M → M → M
    [ x ,, y ] = pr1 (∞-unordered-pairs x y)

-- We construct ordered pairs from the empty set, singletons and unordered pairs
equiv-coprod-equiv-pair-eq : {x x' y y' : M}
                           → ¬ (x == y')
                           → ¬ (x' == y)
                           → ((z : M) → ((x == z) + (y == z)) ≃ ((x' == z) + (y' == z)))
                           ≃ ((x == x') × (y == y'))
equiv-coprod-equiv-pair-eq {x} {x'} {y} {y'} x≠y' x'≠y =
  equivalence-reasoning
    ((z : M) → ((x == z) + (y == z)) ≃ ((x' == z) + (y' == z)))

      ≃ ((z : M) → ((x == z) ≃ (x' == z)) × ((y == z) ≃ (y' == z))) by equiv-Π-equiv-family (λ z →
                                                                         equiv-mutually-exclusive-coprod
                                                                           (λ x=z y'=z → x≠y' (x=z ∙ inv y'=z))
                                                                           (λ x'=z y=z → x'≠y (x'=z ∙ inv y=z)))
      ≃ ((z : M) → (x == z) ≃ (x' == z)) ×
        ((z : M) → (y == z) ≃ (y' == z))                            by distributive-Π-Σ

      ≃ (x == x') × (y == y')                                       by equiv-prod
                                                                         (equiv-inv x' x ∘e equiv-concat-equiv)
                                                                         (equiv-inv y' y ∘e equiv-concat-equiv)

module unordered-pair'-eq
  (unordered-pairs' : UnorderedPairs') where

  open unordered-pairs'.notation unordered-pairs'

  equiv-unordered-pair-eq : {x x' y y' : M}
                          → ¬ (x == y)
                          → ¬ (x' == y')
                          → ¬ (x == y')
                          → ¬ (x' == y)
                          → ([ x ,, y ]' == [ x' ,, y' ]')
                          ≃ ((x == x') × (y == y'))
  equiv-unordered-pair-eq {x} {x'} {y} {y'} x≠y x'≠y' x≠y' x'≠y =
    equivalence-reasoning
      [ x ,, y ]' == [ x' ,, y' ]'

        ≃ ((z : M) → (z ∈ [ x ,, y ]') ≃ (z ∈ [ x' ,, y' ]'))         by equiv-extensionality

        ≃ ((z : M) → ((x == z) + (y == z)) ≃ ((x' == z) + (y' == z))) by equiv-Π-equiv-family (λ z →
                                                                           equiv-postcomp-equiv
                                                                             (pr2 (unordered-pairs' x' y') x'≠y' z)
                                                                             _ ∘e
                                                                           equiv-precomp-equiv
                                                                             (inv-equiv (pr2 (unordered-pairs' x y) x≠y z))
                                                                             _)
        ≃ (x == x') × (y == y')                                       by equiv-coprod-equiv-pair-eq x≠y' x'≠y

  compute-equiv-unordered-pair-eq : {x y : M}
                                  → (x≠y : ¬ (x == y))
                                  → map-equiv (equiv-unordered-pair-eq x≠y x≠y x≠y x≠y) refl
                                  == (refl , refl)
  compute-equiv-unordered-pair-eq {x} {y} x≠y =
    ap (map-equiv
          (equiv-coprod-equiv-pair-eq x≠y x≠y))
       (eq-htpy (λ z →
          eq-htpy-equiv
            {e = pr2 (unordered-pairs' x y) x≠y z ∘e inv-equiv (pr2 (unordered-pairs' x y) x≠y z)}
            {e' = id-equiv}
            (is-section-map-inv-equiv
              (pr2 (unordered-pairs' x y) x≠y z))))

-- The function x ↦ [x] is an embedding
module emb-singleton
  (∞-singletons : ∞-Singletons) where

  open ∞-singletons.notation ∞-singletons

  equiv-singleton-eq : (x x' : M)
                     → ([ x ] == [ x' ])
                     ≃ (x == x')
  equiv-singleton-eq x x' =
    equivalence-reasoning
      [ x ] == [ x' ]

        ≃ ((y : M) → (y ∈ [ x ]) ≃ (y ∈ [ x' ])) by equiv-extensionality

        ≃ ((y : M) → (x == y) ≃ (x' == y))       by equiv-Π-equiv-family (λ y →
                                                      equiv-postcomp-equiv (pr2 (∞-singletons x') y) _ ∘e
                                                      equiv-precomp-equiv (inv-equiv (pr2 (∞-singletons x) y)) _)
        ≃ x' == x                                by equiv-concat-equiv

        ≃ x == x'                                by equiv-inv x' x

  compute-equiv-singleton-eq : (x : M)
                             → map-equiv (equiv-singleton-eq x x) refl
                             == refl
  compute-equiv-singleton-eq x =
    ap (inv ∘ map-equiv equiv-concat-equiv)
       (eq-htpy λ y →
         eq-htpy-equiv
           {e = pr2 (∞-singletons x) y ∘e inv-equiv (pr2 (∞-singletons x) y)}
           {e' = id-equiv}
           (is-section-map-inv-equiv (pr2 (∞-singletons x) y)))

  is-emb-singleton : is-emb [_]
  is-emb-singleton =
    is-emb-equiv-refl-to-refl
      [_]
      equiv-singleton-eq
      compute-equiv-singleton-eq

  emb-singleton : M ↪ M
  pr1 emb-singleton = [_]
  pr2 emb-singleton = is-emb-singleton

-- The function x ↦ [[x],∅] is an embedding
module emb-unordered-pair-singleton-empty
  (empty-set : EmptySet)
  (∞-singletons : ∞-Singletons)
  (unordered-pairs' : UnorderedPairs') where

  open empty-set.properties empty-set
  open empty-set.notation empty-set
  open ∞-singletons.notation ∞-singletons
  open unordered-pairs'.notation unordered-pairs'

  open unordered-pair'-eq unordered-pairs'
  open emb-singleton ∞-singletons

  [_]≠∅ : (x : M) → ¬ ([ x ] == ∅)
  [ x ]≠∅ [x]=∅ =
    map-equiv
      (pr2 empty-set x)
      (tr (x ∈_) [x]=∅
          (map-inv-equiv (pr2 (∞-singletons x) x) refl))

  equiv-unordered-pair-singleton-empty-eq : (x x' : M)
                                          → ([ [ x ] ,, ∅ ]' == [ [ x' ] ,, ∅ ]')
                                          ≃ (x == x')
  equiv-unordered-pair-singleton-empty-eq x x' =
    equivalence-reasoning
      [ [ x ] ,, ∅ ]' == [ [ x' ] ,, ∅ ]'

        ≃ ([ x ] == [ x' ]) × (∅ == ∅)  by equiv-unordered-pair-eq [ x ]≠∅ [ x' ]≠∅ [ x ]≠∅ [ x' ]≠∅

        ≃ ([ x ] == [ x' ])               by right-unit-law-prod-is-contr
                                               (is-proof-irrelevant-is-prop
                                                 (is-prop-eq-mere-set
                                                   mere-set-empty-set)
                                                 refl)
        ≃ x == x'                         by inv-equiv (equiv-ap-emb emb-singleton)

  compute-equiv-unordered-pair-singleton-empty-eq : (x : M)
                                                  → map-equiv (equiv-unordered-pair-singleton-empty-eq x x) refl
                                                  == refl
  compute-equiv-unordered-pair-singleton-empty-eq x =
    equational-reasoning
      map-equiv (equiv-unordered-pair-singleton-empty-eq x x) refl

        ＝ map-inv-equiv (equiv-ap-emb emb-singleton) refl         by ap (map-inv-equiv (equiv-ap-emb emb-singleton) ∘ pr1)
                                                                         (compute-equiv-unordered-pair-eq [ x ]≠∅)
        ＝ refl                                                    by is-retraction-map-inv-equiv
                                                                       (equiv-ap-emb emb-singleton)
                                                                       refl

  is-emb-unordered-pair-singleton-empty : is-emb (λ x → [ [ x ] ,, ∅ ]')
  is-emb-unordered-pair-singleton-empty =
    is-emb-equiv-refl-to-refl
      (λ x → [ [ x ] ,, ∅ ]')
      equiv-unordered-pair-singleton-empty-eq
      compute-equiv-unordered-pair-singleton-empty-eq

  emb-unordered-pair-singleton-empty : M ↪ M
  pr1 emb-unordered-pair-singleton-empty = (λ x → [ [ x ] ,, ∅ ]')
  pr2 emb-unordered-pair-singleton-empty = is-emb-unordered-pair-singleton-empty

  [[_],,∅]≠[[_]] : (x y : M) → ¬ ([ [ x ] ,, ∅ ]' == [ [ y ] ])
  [[ x ],,∅]≠[[ y ]] [[x],,∅]=[[y]] = [ y ]≠∅ [y]=∅
    where
      ∅∈[[y]] : ∅ ∈ [ [ y ] ]
      ∅∈[[y]] =
        tr (∅ ∈_) [[x],,∅]=[[y]]
           (map-inv-equiv
             (pr2 (unordered-pairs' [ x ] ∅) [ x ]≠∅ ∅)
             (inr refl))

      [y]=∅ : [ y ] == ∅
      [y]=∅ = map-equiv (pr2 (∞-singletons [ y ]) ∅) ∅∈[[y]]

module ordered-pairs where

  open e-structure.core.ordered-pairing-structure M

  -- Given two distinct embeddings and unordered pairs we can construct ordered pairs
  module from-distinct-embeddings
    (f : M ↪ M) (g : M ↪ M)
    (f≠g : (x y : M) → ¬ (f 〈 x 〉 == g 〈 y 〉))
    (unordered-pairs' : UnorderedPairs') where

    open unordered-pair'-eq unordered-pairs'

    ordered-pair : M → M → M
    ordered-pair x y = pr1 (unordered-pairs' (f 〈 x 〉) (g 〈 y 〉))

    equiv-ordered-pair-eq : (x x' y y' : M)
                          → (ordered-pair x y == ordered-pair x' y')
                          ≃ ((x , y) == (x' , y'))
    equiv-ordered-pair-eq x x' y y' =
      equivalence-reasoning
        ordered-pair x y == ordered-pair x' y'

          ≃ (f 〈 x 〉 == f 〈 x' 〉) × (g 〈 y 〉 == g 〈 y' 〉) by equiv-unordered-pair-eq
                                                                    (f≠g x y)
                                                                    (f≠g x' y')
                                                                    (f≠g x y')
                                                                    (f≠g x' y)
          ≃ (x == x') × (y == y')                              by equiv-prod
                                                                    (inv-equiv (equiv-ap-emb f))
                                                                    (inv-equiv (equiv-ap-emb g))
          ≃ (x , y) == (x' , y')                               by equiv-eq-pair (x , y) (x' , y')

    compute-equiv-ordered-pair-eq : (x y : M)
                                  → map-equiv (equiv-ordered-pair-eq x x y y) refl
                                  == refl
    compute-equiv-ordered-pair-eq x y =
      equational-reasoning
        map-equiv (equiv-ordered-pair-eq x x y y) refl
          ＝ eq-pair'
              (map-inv-equiv (equiv-ap-emb f) refl ,
               map-inv-equiv (equiv-ap-emb g) refl)    by ap (map-equiv
                                                                (equiv-eq-pair (x , y) (x , y) ∘e
                                                                 equiv-prod
                                                                   (inv-equiv (equiv-ap-emb f))
                                                                   (inv-equiv (equiv-ap-emb g))))
                                                             (compute-equiv-unordered-pair-eq (f≠g x y))
          ＝ refl                                      by ap eq-pair'
                                                              (eq-pair'
                                                                (is-retraction-map-inv-equiv (equiv-ap-emb f) refl ,
                                                                is-retraction-map-inv-equiv (equiv-ap-emb g) refl))

    is-emb-ordered-pair : is-emb {A = M × M} (λ (x , y) → ordered-pair x y)
    is-emb-ordered-pair =
      is-emb-equiv-refl-to-refl
        (λ (x , y) → ordered-pair x y)
        (λ (x , y) (x' , y') → equiv-ordered-pair-eq x x' y y')
        (λ (x , y) → compute-equiv-ordered-pair-eq x y)

    ordered-pairs : OrderedPairs
    pr1 ordered-pairs (x , y) = ordered-pair x y
    pr2 ordered-pairs = is-emb-ordered-pair

  -- We construct ordered pairs from unordered tupling
  module from-unordered-pairs'
    (empty-set : EmptySet)
    (∞-singletons : ∞-Singletons)
    (unordered-pairs' : UnorderedPairs') where

    open emb-singleton ∞-singletons
    open emb-unordered-pair-singleton-empty empty-set ∞-singletons unordered-pairs'

    open from-distinct-embeddings
      emb-unordered-pair-singleton-empty
      (comp-emb emb-singleton emb-singleton)
      [[_],,∅]≠[[_]]
      unordered-pairs'
      using (ordered-pairs) public

  module from-∞-unordered-pairs
    (empty-set : EmptySet)
    (∞-singletons : ∞-Singletons)
    (∞-unordered-pairs : ∞-UnorderedPairs) where

    private
      unordered-pairs' : UnorderedPairs'
      pr1 (unordered-pairs' x y) = pr1 (∞-unordered-pairs x y)
      pr2 (unordered-pairs' x y) _ = pr2 (∞-unordered-pairs x y)

    open emb-singleton ∞-singletons
    open emb-unordered-pair-singleton-empty empty-set ∞-singletons unordered-pairs'

    open from-distinct-embeddings
      emb-unordered-pair-singleton-empty
      (comp-emb emb-singleton emb-singleton)
      [[_],,∅]≠[[_]]
      unordered-pairs'
      using (ordered-pairs) public

  -- We construct ordered pair for ∈-structures based on their level
  open e-structure.core.trunc-sets ((M , _∈_) , p)

  ordered-pairs-from-level : (n : ℕ)
                           → ∈-str-has-level n
                           → EmptySet
                           → [ n ]-Singletons
                           → [ n ]-UnorderedPairs
                           → OrderedPairs
  ordered-pairs-from-level zero-ℕ H empty-set n-singletons n-unordered-pairs
    = ordered-pairs where
      M-Set : Set i
      pr1 M-Set = M
      pr2 M-Set = is-trunc-∈-str-carrier zero-ℕ H

      ∞-singletons : ∞-Singletons
      pr1 (∞-singletons x) = pr1 (n-singletons x)
      pr2 (∞-singletons x) z =
        inv-equiv (equiv-unit-trunc (Id-Prop M-Set x z))
        ∘e pr2 (n-singletons x) z

      unordered-pairs' : UnorderedPairs'
      pr1 (unordered-pairs' x y) = pr1 (n-unordered-pairs x y)
      pr2 (unordered-pairs' x y) x≠y z =
        inv-equiv (equiv-unit-trunc
          (coprod-Prop
            (Id-Prop M-Set x z)
            (Id-Prop M-Set y z)
            (λ x=z y=z → x≠y (x=z ∙ inv y=z))))
        ∘e pr2 (n-unordered-pairs x y) z

      open from-unordered-pairs'
             empty-set
             ∞-singletons
             unordered-pairs'

  ordered-pairs-from-level (succ-ℕ n) H empty-set n-singletons n-unordered-pairs
    = ordered-pairs where
      M-Truncated-Type : Truncated-Type i (to-𝕋 (succ-ℕ n))
      pr1 M-Truncated-Type = M
      pr2 M-Truncated-Type = is-trunc-∈-str-carrier (succ-ℕ n) H

      ∞-singletons : ∞-Singletons
      pr1 (∞-singletons x) = pr1 (n-singletons x)
      pr2 (∞-singletons x) z =
        inv-equiv (equiv-unit-trunc (Id-Truncated-Type M-Truncated-Type x z))
        ∘e pr2 (n-singletons x) z

      ∞-unordered-pairs : ∞-UnorderedPairs
      pr1 (∞-unordered-pairs x y) = pr1 (n-unordered-pairs x y)
      pr2 (∞-unordered-pairs x y) z =
        inv-equiv (equiv-unit-trunc
          ((x == z) + (y == z) ,
          is-trunc-coprod (minus-two n)
            (pr2 M-Truncated-Type x z)
            (pr2 M-Truncated-Type y z)))
        ∘e pr2 (n-unordered-pairs x y) z

      open from-∞-unordered-pairs
             empty-set
             ∞-singletons
             ∞-unordered-pairs