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

open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.families-of-equivalences
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.propositions
open import foundation.subtypes
open import foundation.truncated-types
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-dependent-pair-types
open import foundation.type-theoretic-principle-of-choice
open import foundation.universal-property-dependent-pair-types
open import foundation.universe-levels

open import notation as N

module e-structure.core where

map-extensionality : {i j : Level} (M : UU i) (_∈_ : M → M → UU j)
                   → {x y : M}
                   → x == y
                   → (z : M) → (z ∈ x) ≃ (z ∈ y)
map-extensionality M _∈_ refl z = id-equiv

module _ {i j} {M : UU i} (_∈_ : M → M → UU j) where

  is-extensional : UU (i ⊔ j)
  is-extensional = {x y : M} → is-equiv (map-extensionality M _∈_ {x} {y})

  is-prop-is-extensional : is-prop is-extensional
  is-prop-is-extensional =
    is-prop-Π' (λ x →
      is-prop-Π' (λ y →
        is-property-is-equiv (map-extensionality M _∈_)))

  is-extensional-Prop : Prop (i ⊔ j)
  pr1 is-extensional-Prop = is-extensional
  pr2 is-extensional-Prop = is-prop-is-extensional

∈-structure : ∀ i j → UU (lsuc i ⊔ lsuc j)
∈-structure i j =
  Σ (Σ (UU i) (λ M → M → M → UU j))
    λ (M , _∈_) → is-extensional _∈_

module extensionality {i j}
  (((M , _∈_) , p) : ∈-structure i j) where

  equiv-extensionality : {x y : M}
                       → (x == y)
                       ≃ ((z : M) → (z ∈ x) ≃ (z ∈ y))
  pr1 equiv-extensionality = map-extensionality M _∈_
  pr2 equiv-extensionality = p

  is-prop-total-space-fixed-∈ : {k : Level} (φ : M → UU k)
                              → is-prop (Σ M λ x → (z : M) → (z ∈ x) ≃ φ z)
  is-prop-total-space-fixed-∈ φ =
    is-prop-is-proof-irrelevant
      (λ (x , α) →
        is-contr-equiv _
          (equiv-tot (λ x' →
            inv-equiv equiv-extensionality
            ∘e equiv-Π-equiv-family (λ z → equiv-postcomp-equiv (inv-equiv (α z)) _)))
          (is-torsorial-path' x))

module trunc-sets {i j}
  (((M , _∈_) , p) : ∈-structure i j) where

  open extensionality ((M , _∈_) , p)

  is-[_]-type : (k : ℕ) → M → UU (i ⊔ j)
  is-[ k ]-type x = (y : M) → is-trunc (minus-one k) (y ∈ x)

  is-prop-is-[_]-type : (k : ℕ) → (x : M) → is-prop (is-[ k ]-type x)
  is-prop-is-[ k ]-type x = is-prop-Π (λ y → is-prop-is-trunc (minus-one k) (y ∈ x))

  is-[_]-type-Prop : ℕ → M → Prop (i ⊔ j)
  pr1 (is-[ k ]-type-Prop x) = is-[ k ]-type x
  pr2 (is-[ k ]-type-Prop x) = is-prop-is-[ k ]-type x

  is-trunc-eq-is-[_]-type' : (k : ℕ)
                        → {x : M} → is-[ k ]-type x
                        → {y : M} → is-trunc (minus-one k) (y == x)
  is-trunc-eq-is-[ k ]-type' k-type-x =
    is-trunc-equiv (minus-one k) _
      equiv-extensionality
      (is-trunc-Π (minus-one k) (λ z →
        is-trunc-Σ
          (is-trunc-function-type (minus-one k) (k-type-x z))
          (λ e → is-trunc-is-prop (minus-two k) (is-property-is-equiv e))))

  is-trunc-eq-is-[_]-type : (k : ℕ)
                            → {x : M} → is-[ k ]-type x
                            → {y : M} → is-trunc (minus-one k) (x == y)
  is-trunc-eq-is-[ k ]-type k-type-x =
    is-trunc-equiv (minus-one k) _
      (equiv-inv _ _)
      (is-trunc-eq-is-[ k ]-type' k-type-x)

  ∈-str-has-level : (k : ℕ) → UU (i ⊔ j)
  ∈-str-has-level k = (x : M) → is-[ k ]-type x

  is-trunc-∈-str-carrier : (k : ℕ)
                         → ∈-str-has-level k
                         → is-trunc (to-ℕ k) M
  is-trunc-∈-str-carrier k H x y = is-trunc-eq-is-[ k ]-type (H x)

module mere-sets {i j}
  (((M , _∈_) , p) : ∈-structure i j) where

  open trunc-sets ((M , _∈_) , p)

  mere-set : M → UU (i ⊔ j)
  mere-set = is-[ zero-ℕ ]-type

  is-prop-mere-set : (x : M) → is-prop (mere-set x)
  is-prop-mere-set = is-prop-is-[ zero-ℕ ]-type

  mere-set-Prop : M → Prop (i ⊔ j)
  mere-set-Prop = is-[ zero-ℕ ]-type-Prop

  is-prop-eq-mere-set' : {x : M} → mere-set x
                       → {y : M} → is-prop (y == x)
  is-prop-eq-mere-set' = is-trunc-eq-is-[ zero-ℕ ]-type'

  is-prop-eq-mere-set : {x : M} → mere-set x
                      → {y : M} → is-prop (x == y)
  is-prop-eq-mere-set = is-trunc-eq-is-[ zero-ℕ ]-type

module elements {i j} ((M , _∈_) : Σ (UU i) (λ M → M → M → UU j)) where

  El : (a : M) → UU (i ⊔ j)
  El a = Σ M (λ x → x ∈ a)

  extensionality-El-equiv : {x y : M}
                          → ((z : M) → (z ∈ x) ≃ (z ∈ y))
                          ≃ Σ (El x ≃ El y) (λ e → (pr1 ∘ map-equiv e) ~ pr1)
  extensionality-El-equiv {x} {y} =
    equivalence-reasoning
      ((z : M) → (z ∈ x) ≃ (z ∈ y))
        ≃ Σ ((z : M) → (z ∈ x) → (z ∈ y))
            is-fiberwise-equiv                               by distributive-Π-Σ
        ≃ Σ (Σ (El x → El y) (λ e → (pr1 ∘ e) ~ pr1))
            (λ (e , _) → is-equiv e)                         by equiv-subtype-equiv
                                                                  α
                                                                  (λ e → Π-Prop M (λ z → is-equiv-Prop (e z)))
                                                                  (λ (e , _) → is-equiv-Prop e)
                                                                  (λ e →
                                                                    is-equiv-tot-is-fiberwise-equiv ,
                                                                    is-fiberwise-equiv-is-equiv-tot)
        ≃ Σ (El x ≃ El y) (λ e → (pr1 ∘ map-equiv e) ~ pr1)  by equiv-right-swap-Σ
    where
    α : ((z : M) → (z ∈ x) → (z ∈ y))
      ≃ Σ (El x → El y) (λ e → (pr1 ∘ e) ~ pr1)
    α =
      equivalence-reasoning
        ((z : M) → (z ∈ x) → (z ∈ y))
          ≃ (((z , _) : El x) → z ∈ y)              by inv-equiv equiv-ev-pair
          ≃ (((z , _) : El x)
            → Σ (Σ M λ z' → z' == z)
                λ (z' , _) → z' ∈ y)                by equiv-Π-equiv-family (λ (z , _) →
                                                         inv-left-unit-law-Σ-is-contr (is-torsorial-path' z) (z , refl))
          ≃ (((z , _) : El x)
            → Σ (El y) λ (z' , _) → z' == z)        by equiv-Π-equiv-family (λ (z , _) → equiv-right-swap-Σ)
          ≃ Σ (El x → El y) (λ e → (pr1 ∘ e) ~ pr1) by distributive-Π-Σ

  compute-extensionality-El-equiv : {x : M}
                                  → map-equiv (extensionality-El-equiv {x} {x}) (λ _ → id-equiv)
                                  == (id-equiv , refl-htpy)
  compute-extensionality-El-equiv =
    ap map-right-swap-Σ
       (eq-type-subtype (is-equiv-Prop ∘ pr1) refl)

module ordered-pairing-structure
  {i} (M : UU i) where

  OrderedPairs : UU i
  OrderedPairs = (M × M) ↪ M

  module notation (ordered-pairs : OrderedPairs) where

    ⟨_,_⟩ : M → M → M
    ⟨ x , y ⟩ = map-emb ordered-pairs (x , y)