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

open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equivalences
open import foundation.equivalence-induction
open import foundation.function-types
open import foundation.functoriality-coproduct-types
open import foundation.functoriality-propositional-truncation
open import foundation.identity-types
open import foundation.injective-maps
open import foundation.propositional-maps
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.truncated-maps
open import foundation.truncation-levels
  renaming (truncation-level-minus-one-ℕ to minus-one)
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.natural-numbers
  {i j} (((M , _∈_) , p) : ∈-structure i j) where

-- Import the notation El
open e-structure.core.elements (M , _∈_)

open import e-structure.internalisations ((M , _∈_) , p)
open import e-structure.property.replacement ((M , _∈_) , p)

NaturalNumbersRepresentedBy : (f : Representation ℕ) → UU (i ⊔ j)
NaturalNumbersRepresentedBy f = InternalisationOfRepr f

all-nats-given-replacement : (k : ℕ)
                           → [ k ]-Replacement
                           → Σ (Representation ℕ) NaturalNumbersRepresentedBy
                           → (f : Representation ℕ)
                           → is-trunc-map (minus-one k) f
                           → NaturalNumbersRepresentedBy f
all-nats-given-replacement k R (f , (n , α)) =
  int-repr-given-replacement k R {A = ℕ}
    (n , (equiv-El-repr-domain (n , α)))

module zero-succ
  (f : Representation ℕ) ((nat , α) : NaturalNumbersRepresentedBy f)
  where

  private
    e : El nat ≃ ℕ
    e = equiv-El-repr-domain (nat , α)

  zero-nat : El nat
  zero-nat = map-inv-equiv e zero-ℕ

  succ-nat : El nat → El nat
  succ-nat = map-inv-equiv e ∘ (succ-ℕ ∘ map-equiv e)

module ind-NaturalNumbers
  (f : Representation ℕ) ((nat , α) : NaturalNumbersRepresentedBy f)
  where

  open zero-succ f (nat , α)

  ind-nat : {k : Level} (P : El nat → UU k)
          → P zero-nat
          → ((x : El nat) → P x → P (succ-nat x))
          → (x : El nat) → P x
  ind-nat P p0 IH x = tr P (is-retraction-map-inv-equiv e x) (ind-nat-aux (map-equiv e x))
    where
      e : El nat ≃ ℕ
      e = equiv-El-repr-domain (nat , α)

      ind-nat-aux : (n : ℕ) → P (map-inv-equiv e n)
      ind-nat-aux zero-ℕ = p0
      ind-nat-aux (succ-ℕ n) =
        tr P
           (ap (map-inv-equiv e ∘ succ-ℕ) (is-section-map-inv-equiv e n))
           (IH (map-inv-equiv e n) (ind-nat-aux n))


{-
Given the empty set, singletons and binary unions
we can define the representation that corresponds
to the von Neumann encoding of the natural numbers.
-}

open import e-structure.property.union ((M , _∈_) , p)
open import e-structure.property.unordered-tupling ((M , _∈_) , p)

module von-neumann
  (empty-set : EmptySet)
  (0-singletons : 0-Singletons)
  (binary-0-union : Binary-0-Union)
  where

  open mere-sets ((M , _∈_) , p)
  open extensionality ((M , _∈_) , p)

  open empty-set.properties empty-set
  open empty-set.notation empty-set
  open 0-singletons.notation 0-singletons
  open binary.notation binary-0-union

  s : M → M
  s x = x ∪ ｛ x ｝

  ∈-s : (x y : M)
      → (y ∈ s x)
      ≃ type-trunc-Prop ((y ∈ x) + type-trunc-Prop (x == y))
  ∈-s x y =
    equivalence-reasoning
      y ∈ s x
        ≃ type-trunc-Prop ((y ∈ x) + (y ∈ ｛ x ｝)) by pr2 (binary-0-union x ｛ x ｝) y
        ≃ type-trunc-Prop
            ((y ∈ x) + type-trunc-Prop (x == y))   by equiv-trunc-Prop
                                                        (equiv-coprod id-equiv (pr2 (0-singletons x) y))

  ∈-s-mere-set : (x y : M)
               → mere-set x
               → (y ∈ s x)
               ≃ type-trunc-Prop ((y ∈ x) + (x == y))
  ∈-s-mere-set x y mere-set-x =
    equivalence-reasoning
      y ∈ s x
      ≃ type-trunc-Prop ((y ∈ x) + type-trunc-Prop (x == y)) by ∈-s x y
      ≃ type-trunc-Prop ((y ∈ x) + (x == y))                 by equiv-trunc-Prop
                                                                  (equiv-coprod id-equiv
                                                                    (inv-equiv (equiv-unit-trunc-Prop
                                                                      (x == y ,
                                                                      is-prop-eq-mere-set mere-set-x))))

  x∈sx : (x : M) → x ∈ s x
  x∈sx x = map-inv-equiv (∈-s x x) (unit-trunc-Prop (inr (unit-trunc-Prop refl)))

  mere-set-s : (x : M) → mere-set (s x)
  mere-set-s x y = is-prop-equiv (∈-s x y) is-prop-type-trunc-Prop

  accessible-s : {x : M} → is-accessible-element-Relation _∈_ x → is-accessible-element-Relation _∈_ (s x)
  accessible-s {x} (access f) =
    access (λ {y} y∈sx →
      map-universal-property-trunc-Prop
        (is-accessible-element-prop-Relation _∈_ y)
        (ind-coprod
          (λ _ → is-accessible-element-Relation _∈_ y)
          (λ y∈x → f y∈x)
          (map-universal-property-trunc-Prop
            (is-accessible-element-prop-Relation _∈_ y)
            (λ x=y → tr (is-accessible-element-Relation _∈_) x=y (access f))))
        (map-equiv (∈-s x y) y∈sx))

  von-neumann-repr : ℕ → M
  von-neumann-repr zero-ℕ = ∅
  von-neumann-repr (succ-ℕ n) = s (von-neumann-repr n)

  mere-set-von-neumann-repr : (n : ℕ) → mere-set (von-neumann-repr n)
  mere-set-von-neumann-repr zero-ℕ = mere-set-empty-set
  mere-set-von-neumann-repr (succ-ℕ n) = mere-set-s (von-neumann-repr n)

  accessible-von-neumann-repr : (n : ℕ) → is-accessible-element-Relation _∈_ (von-neumann-repr n)
  accessible-von-neumann-repr zero-ℕ =
    access (λ {y} y∈∅ → ex-falso (map-equiv (pr2 empty-set y) y∈∅))
  accessible-von-neumann-repr (succ-ℕ n) =
    accessible-s (accessible-von-neumann-repr n)

  is-inj-s : {x y : M}
           → is-accessible-element-Relation _∈_ x
           → mere-set x → mere-set y
           → s x == s y
           → x == y
  is-inj-s {x} {y} accessible-x mere-set-x mere-set-y sx=sy =
    map-universal-property-trunc-Prop
      (x == y , is-prop-eq-mere-set mere-set-x)
      (ind-coprod
        (λ _ → x == y)
        (λ x∈y →
          map-universal-property-trunc-Prop
            (x == y , is-prop-eq-mere-set mere-set-x)
            (ind-coprod
              (λ _ → x == y)
              (λ y∈x → ex-falso (is-asymmetric-is-accessible-element-Relation _∈_ accessible-x x∈y y∈x))
              id)
            (map-inv-equiv (ϕ y) (unit-trunc-Prop (inr refl))))
        inv)
      (map-equiv (ϕ x) (unit-trunc-Prop (inr refl)))
    where
      ϕ : (z : M)
        → type-trunc-Prop ((z ∈ x) + (x == z))
        ≃ type-trunc-Prop ((z ∈ y) + (y == z))
      ϕ z = ∈-s-mere-set y z mere-set-y
        ∘e (map-equiv equiv-extensionality sx=sy z
        ∘e inv-equiv (∈-s-mere-set x z mere-set-x))

  is-inj-von-neumann-repr : is-injective von-neumann-repr
  is-inj-von-neumann-repr {zero-ℕ} {zero-ℕ} ∅=∅ = refl
  is-inj-von-neumann-repr {zero-ℕ} {succ-ℕ n} ∅=sn =
    ex-falso
      (map-equiv (pr2 empty-set (von-neumann-repr n))
        (inv-tr (von-neumann-repr n ∈_) ∅=sn (x∈sx (von-neumann-repr n))))
  is-inj-von-neumann-repr {succ-ℕ m} {zero-ℕ} sm=∅ =
    ex-falso
      (map-equiv (pr2 empty-set (von-neumann-repr m))
        (tr (von-neumann-repr m ∈_) sm=∅ (x∈sx (von-neumann-repr m))))
  is-inj-von-neumann-repr {succ-ℕ m} {succ-ℕ n} sm=sn =
    ap succ-ℕ
       (is-inj-von-neumann-repr {m} {n}
         (is-inj-s
           (accessible-von-neumann-repr m)
           (mere-set-von-neumann-repr m)
           (mere-set-von-neumann-repr n)
           sm=sn))

  is-prop-map-von-neumann-repr : is-prop-map von-neumann-repr
  is-prop-map-von-neumann-repr z =
    is-prop-all-elements-equal (λ (m , s) (n , t) →
      eq-type-subtype
        (λ n' → (von-neumann-repr n' == z ,
                is-prop-eq-mere-set (mere-set-von-neumann-repr n')))
        (is-inj-von-neumann-repr (s ∙ inv t)))

  is-emb-von-neumann-repr : is-emb von-neumann-repr
  is-emb-von-neumann-repr = is-emb-is-prop-map is-prop-map-von-neumann-repr