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

open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.locally-small-types
open import foundation.propositional-maps
open import foundation.raising-universe-levels
open import foundation.truncated-maps
open import foundation.truncation-levels
  renaming (truncation-level-minus-one-ℕ to minus-one;
    truncation-level-minus-two-ℕ to minus-two)
open import foundation.univalence
open import foundation.universe-levels

open import e-structure.core
open import functor.n-slice
open import image-factorisation
open import notation hiding (sup)

module fixed-point.natural-numbers {i j} (n : ℕ)
  (V : UU j) (fixed-point-V : V ≃ T-[ n ] i V) where

-- Construction of ∈-structure on V
open import fixed-point.core n V fixed-point-V

-- Property of having a natural numbers set with respect to a presentation
open import e-structure.property.natural-numbers ∈-structure-V
-- Internalisations and representations
open import e-structure.internalisations ∈-structure-V

-- V has natural numbers with respect to any (n-1)-truncated representation
module _
  (f : Representation ℕ)
  (p : is-trunc-map (minus-one n) f)
  where

  nat : V
  nat =
    sup (raise i ℕ ,
        comp-trunc-map (minus-one n)
          (f , p)
          (map-inv-raise ,
          is-trunc-map-is-equiv (minus-one n)
            (is-equiv-map-inv-equiv (compute-raise i ℕ))))

  natural-numbers-trunc-repr : NaturalNumbersRepresentedBy f
  pr1 natural-numbers-trunc-repr = nat
  pr2 natural-numbers-trunc-repr z =
    equivalence-reasoning
      z ∈ nat
      ≃ Σ (raise i ℕ) (λ n →
          f (map-inv-raise n) == z) by equiv-eq (∈-sup z)
      ≃ fiber f z                     by equiv-Σ-equiv-base _ (inv-equiv (compute-raise i ℕ))

-- In particular, we have natural numbers with respect
-- to the von Neumann encoding, if V is locally small
module _ (p : is-locally-small i V) where

  open import fixed-point.empty-set n V fixed-point-V
  open import fixed-point.unordered-tupling n zero-ℕ n refl V fixed-point-V p
  open import fixed-point.union n zero-ℕ n refl V fixed-point-V p

  open von-neumann empty-set singletons binary-union

  natural-numbers-von-neumann : NaturalNumbersRepresentedBy von-neumann-repr
  natural-numbers-von-neumann =
    natural-numbers-trunc-repr
      von-neumann-repr
      (is-trunc-map-is-prop-map (minus-two n) is-prop-map-von-neumann-repr)