iterative.set

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

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.inequality-natural-numbers
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.coherently-invertible-maps
open import foundation.dependent-pair-types
open import foundation.dependent-universal-property-equivalences
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.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.equivalence-induction
open import foundation.families-of-maps
open import foundation.fibers-of-maps
open import foundation.function-extensionality
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.images
open import foundation.injective-maps
open import foundation.monomorphisms
open import foundation.negated-equality
open import foundation.propositional-maps
open import foundation.propositions
open import foundation.raising-universe-levels
open import foundation.sets
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;
    truncation-level-minus-two-ℕ to minus-two)
open import foundation.unit-type
open import foundation.univalence
open import foundation.universe-levels
open import foundation.locally-small-types

open import functor.n-slice
open import functor.slice
open import image-factorisation
open import notation
open import set-quotient


module iterative.set where

{- V∞ is the unrestricted iterative hiearchy -}
V∞ : ∀ i → UU (lsuc i)
V∞ i = W (UU i) id

desup∞ : ∀ {i} → V∞ i → T∞ i (V∞ i)
desup∞ (sup A f) = (A , f)

{- The underlying type of an element in V∞ -}
El∞ : ∀ {i} → V∞ i → UU i
El∞ x = ¦ desup∞ x ¦

{- Equality on V∞ is defined as equivalences
   of the underlying types which commute with
   the indexing function -}

infix 100 _==V∞_

_==V∞_ : ∀ {i} → V∞ i → V∞ i → UU i
(sup A f) ==V∞ (sup B g) = Σ (A ≃ B) λ α → ∀ x → f x ==V∞ (g (α 〈 x 〉))

equiv-Eq-V∞ : ∀ {i} (x y : V∞ i)
            → (x ==W y) ≃ (x ==V∞ y)
equiv-Eq-V∞ (sup A f) (sup B g)
   = equiv-Σ _
         equiv-univalence
         (λ {refl → equiv-Π-equiv-family (λ a → equiv-Eq-V∞ _ _) })

equiv-eq-V∞ : ∀ {i} (x y : V∞ i)
            → (x == y) ≃ (x ==V∞ y)
equiv-eq-V∞ x y = (equiv-Eq-V∞ _ _) ∘e  (equiv-Eq-𝕎-eq _ _)


{- The n-iterative sets in V∞ are those for which
   the indexing function is an n-truncated map on all levels. -}

is-[_]-iterative-set : ∀ {i} → 𝕋 → V∞ i → UU (lsuc i)
is-[ n ]-iterative-set (sup A f) =
  is-trunc-map n f × ((a : A) → is-[ n ]-iterative-set (f a))

is-prop-is-[_]-iterative-set : ∀ {i} (n : 𝕋) (x : V∞ i) → is-prop (is-[ n ]-iterative-set x)
is-prop-is-[ n ]-iterative-set (sup A f)
  = is-prop-prod (is-prop-is-trunc-map n f) (is-prop-Π λ x → is-prop-is-[ n ]-iterative-set _)


is-[_]-iterative-set-Prop : ∀ {i} → 𝕋 → V∞ i → Prop (lsuc i)
pr1 (is-[ n ]-iterative-set-Prop x) = is-[ n ]-iterative-set x
pr2 (is-[ n ]-iterative-set-Prop x) = is-prop-is-[ n ]-iterative-set x


{- V-[n] is the subtype of V∞ of [n-1]-iterative sets. -}
V-[_] : ℕ → (i : Level) → UU (lsuc i)
V-[ n ] i = Σ (V∞ i) is-[ minus-one n ]-iterative-set

{- Synonyms for some special cases -}

V⁰ : ∀ i → UU (lsuc i)
V⁰ i = V-[ 0 ] i

V¹ : ∀ i → UU (lsuc i)
V¹ i = V-[ 1 ] i

{- Inclusion of Vⁿ into V∞ -}

V-[_]↪V∞ : ∀ {i} (n : ℕ) → V-[ n ] i ↪ V∞ i
V-[ n ]↪V∞ = emb-subtype is-[ minus-one n ]-iterative-set-Prop

V⁰↪V∞ : ∀ {i} → V⁰ i ↪ V∞ i
V⁰↪V∞ = V-[ 0 ]↪V∞

is-trunc-map-V-[_]↪V∞ : ∀ {i} (n : ℕ)
                      → is-trunc-map (minus-one n) (map-emb (V-[_]↪V∞ {i} n))
is-trunc-map-V-[ n ]↪V∞ =
  is-trunc-map-is-prop-map
    (minus-two n)
    (is-prop-map-is-emb
      (is-emb-map-emb V-[ n ]↪V∞))

Eq-V : ∀ {i} (n : ℕ) → V-[ n ] i → V-[ n ] i → UU i
Eq-V n x y = V-[ n ]↪V∞ 〈 x 〉 ==V∞ V-[ n ]↪V∞ 〈 y 〉

syntax Eq-V n x y = x ==V-[ n ] y

equiv-eq-Eq-V : ∀ {i} {n : ℕ} (x y : V-[ n ] i)
              → (x == y) ≃ (x ==V-[ n ] y)
equiv-eq-Eq-V {n = n} x y =
  equiv-eq-V∞ (pr1 x) (pr1 y) ∘e
  extensionality-type-subtype' is-[ minus-one n ]-iterative-set-Prop x y

is-locally-small-V : ∀ {i} {n : ℕ} → is-locally-small i (V-[ n ] i)
pr1 (is-locally-small-V {n = n} x y) = x ==V-[ n ] y
pr2 (is-locally-small-V x y) = equiv-eq-Eq-V x y

is-locally-small-V⁰ : ∀ {i} → is-locally-small i (V⁰ i)
is-locally-small-V⁰ = is-locally-small-V


is-[succ-ℕ_]-small-V : ∀ {i} {n : ℕ} (k : ℕ) → is-[ succ-ℕ k ]-small i (V-[ n ] i)
is-[succ-ℕ k ]-small-V =
  is-[succ-ℕ k ]-small-is-locally-small is-locally-small-V

{- sup-[ n ] and desup-[ n ] defined below make V-[ n ] into a fixed
   point for T-[ n ] i -}

sup-[_] : ∀ {i} (n : ℕ) → T-[ n ] i (V-[ n ] i) → V-[ n ] i
pr1 (sup-[ n ] (A , f)) = sup A (map-emb V-[ n ]↪V∞ ∘ map-trunc-map f)
pr1 (pr2 (sup-[ n ] (A , f))) =
  is-trunc-map-comp
    (minus-one n)
    (map-emb V-[ n ]↪V∞)
    (map-trunc-map f)
    (is-trunc-map-V-[ n ]↪V∞)
    (pr2 f)
pr2 (pr2 (sup-[ n ] (A , f))) a = pr2 (f 〈 a 〉)

-- Some special cases
sup⁰ : ∀ {i} → T⁰ i (V⁰ i) → V⁰ i
sup⁰ = sup-[ 0 ]

-- For V⁰ we may equivalently construct an element from
-- a small type and an embedding into V⁰
sup⁰' : ∀ {i} → Σ (UU i) (λ A → A ↪ V⁰ i) → V⁰ i
sup⁰' (A , f) = sup⁰ (A , (map-emb f , is-prop-map-is-emb (is-emb-map-emb f)))

sup¹ : ∀ {i} → T¹ i (V¹ i) → V¹ i
sup¹ = sup-[ 1 ]

desup-[_] : ∀ {i} (n : ℕ) → V-[ n ] i → T-[ n ] i (V-[ n ] i)
pr1 (desup-[ n ] (sup A f , p)) = A
pr1 (pr2 (desup-[ n ] (sup A f , p))) a = (f a , pr2 p a)
pr2 (pr2 (desup-[ n ] (sup A f , p))) =
  is-trunc-map-right-factor
    (minus-one n)
    (map-emb V-[ n ]↪V∞)
    (λ a → f a , pr2 p a)
    (is-trunc-map-V-[ n ]↪V∞)
    (pr1 p)

-- Some special cases
desup⁰ : ∀ {i} → V⁰ i → T⁰ i (V⁰ i)
desup⁰ = desup-[ 0 ]

desup¹ : ∀ {i} → V¹ i → T¹ i (V¹ i)
desup¹ = desup-[ 1 ]

{- The underlying type of an element in Vⁿ -}

El-[_] : ∀ {i} (n : ℕ) → V-[ n ] i → UU i
El-[ n ] x = ¦ desup-[ n ] x ¦

El⁰ : ∀ {i} → V⁰ i → UU i
El⁰ = El-[ 0 ]

El¹ : ∀ {i} → V¹ i → UU i
El¹ = El-[ 1 ]


V-T-[_]-Coalg : (n : ℕ) → (i : Level) → T-[ n ]-Coalg i (lsuc i)
pr1 (V-T-[ n ]-Coalg i) = V-[ n ] i
pr2 (V-T-[ n ]-Coalg i) = desup-[ n ]

-- Some special cases
V⁰-T⁰-Coalg : ∀ i → T⁰-Coalg i (lsuc i)
V⁰-T⁰-Coalg = V-T-[ 0 ]-Coalg

V¹-T¹-Coalg : ∀ i → T¹-Coalg i (lsuc i)
V¹-T¹-Coalg = V-T-[ 1 ]-Coalg

V-T-[_]-Alg : (n : ℕ) → (i : Level) → T-[ n ]-Alg i (lsuc i)
pr1 (V-T-[ n ]-Alg i) = V-[ n ] i
pr2 (V-T-[ n ]-Alg i) = sup-[ n ]

-- Some special cases
V⁰-T⁰-Alg : ∀ i → T⁰-Alg i (lsuc i)
V⁰-T⁰-Alg = V-T-[ 0 ]-Alg

V¹-T¹-Alg : ∀ i → T¹-Alg i (lsuc i)
V¹-T¹-Alg = V-T-[ 1 ]-Alg

sup-desup-[_] : ∀ {i} (n : ℕ) (x : V-[ n ] i)
              → sup-[ n ] (desup-[ n ] x) == x
sup-desup-[ n ] (sup A f , p) =
  eq-type-subtype
    is-[ minus-one n ]-iterative-set-Prop
    refl

desup-sup-[_] : ∀ {i} (n : ℕ) (x : T-[ n ] i (V-[ n ] i))
              → desup-[ n ] (sup-[ n ] x) == x
desup-sup-[ n ] (A , f) =
  eq-pair-Σ
    refl
    (eq-type-subtype
      (is-trunc-map-Prop (minus-one n))
      refl)

sup-[_]-equiv : (n : ℕ) {i : Level}
              → T-[ n ] i (V-[ n ] i) ≃ V-[ n ] i
pr1 sup-[ n ]-equiv = sup-[ n ]
pr2 sup-[ n ]-equiv =
  is-equiv-is-invertible desup-[ n ] sup-desup-[ n ] desup-sup-[ n ]

-- Some special cases
sup⁰-equiv : ∀ {i} → T⁰ i (V⁰ i) ≃ V⁰ i
sup⁰-equiv = sup-[ 0 ]-equiv

sup¹-equiv : ∀ {i} → T¹ i (V¹ i) ≃ V¹ i
sup¹-equiv = sup-[ 1 ]-equiv

desup-[_]-equiv : (n : ℕ) {i : Level}
                → V-[ n ] i ≃ T-[ n ] i (V-[ n ] i)
pr1 desup-[ n ]-equiv = desup-[ n ]
pr2 desup-[ n ]-equiv =
  is-equiv-is-invertible sup-[ n ] desup-sup-[ n ] sup-desup-[ n ]

-- Some special cases
desup⁰-equiv : ∀ {i} → V⁰ i ≃ T⁰ i (V⁰ i)
desup⁰-equiv = desup-[ 0 ]-equiv

desup¹-equiv : ∀ {i} → V¹ i ≃ T¹ i (V¹ i)
desup¹-equiv = desup-[ 1 ]-equiv

{- A few different elimination and recursion principles
   for V⁰ -}

{- V-[ n ]-elim is the expected elimination principle
   if we regard sup-[ n ] as a constructor -}

V-[_]-elim : ∀ {i j}
           → (n : ℕ)
           → (P : V-[ n ] i → UU j)
           → (∀ A f → ((a : A) → P (f 〈 a 〉)) → P (sup-[ n ] (A , f)))
           → (x : V-[ n ] i) → P x
V-[ n ]-elim P H x@(sup A f , (p₁ , p₂)) =
  let f' = pr2 (desup-[ n ] x) in
  tr P
     (sup-desup-[ n ] x)
     (H A f' (λ a → V-[ n ]-elim P H (f a , p₂ a)))

-- Some special cases
V⁰-elim : ∀ {i j}
        → (P : V⁰ i → UU j)
        → (∀ A f → (∀ a → P (f 〈 a 〉)) → P (sup⁰ (A , f)))
        → ∀ x → P x
V⁰-elim = V-[ 0 ]-elim

V¹-elim : ∀ {i j}
        → (P : V¹ i → UU j)
        → (∀ A f → (∀ a → P (f 〈 a 〉)) → P (sup¹ (A , f)))
        → ∀ x → P x
V¹-elim = V-[ 1 ]-elim

-- The computation rule for V-[ n ]-elim holds only up to homotopy
V-[_]-elim-comp : (n : ℕ)
           → {i j : Level}
           → (P : V-[ n ] i → UU j)
           → (H : ∀ A f → (∀ a → P (f 〈 a 〉)) → P (sup-[ n ] (A , f)))
           → ∀ A f
           → V-[ n ]-elim P H (sup-[ n ] (A , f)) == H A f (V-[ n ]-elim P H ∘ map-trunc-map f)
V-[ n ]-elim-comp {i} P H A f =
  ind-equiv
    (λ B e
       → (q : ∀ b → P (pr2 (pr2 e) 〈 b 〉))
       → (b : B)
       → tr P (pr2 (pr2 (pr2 e)) (pr2 (pr2 e) 〈 b 〉)) (q (pr1 e (pr2 (pr2 e) 〈 b 〉))) == q b)
    (λ q b → refl)
    (desup-[ n ]-equiv)
    (λ (A' , f') → H A' f' (V-[ n ]-elim P H ∘ map-trunc-map f'))
    (A , f)

-- Recursion principle into T∞-algebras, uncurried
V-[_]-T∞-rec : (n : ℕ)
             → {i j : Level}
             → (X : UU j)
             → ((A : UU i) → (A → X) → X)
             → V-[ n ] i → X
V-[ n ]-T∞-rec X m (sup A f , (p₁ , p₂)) =
  m A (λ a → V-[ n ]-T∞-rec X m (f a , p₂ a))

-- Recursion principle into Tⁿ-algebras, uncurried
V-[_]-T-rec : (n : ℕ)
            → {i j : Level}
            → (X : UU j)
            → is-[ succ-ℕ n ]-small i X
            → (T-[ n ] i X → X)
            → V-[ n ] i → X
V-[ n ]-T-rec X p m =
  V-[ n ]-T∞-rec X (λ A f → m (trunc-Image p f , trunc-image-inclusion p f))

-- Recursion principle into Tⁿ-algebras
V-[_]-T-Alg-rec : (n : ℕ)
                → {i j : Level}
                → (X : T-[ n ]-Alg i j)
                → (p : is-[ succ-ℕ n ]-small i ¦ X ¦)
                → hom-T-[ n ]-Alg (V-T-[ n ]-Alg i) X p
pr1 (V-[ n ]-T-Alg-rec X p) = V-[ n ]-T-rec ¦ X ¦ p (X ↓)
pr2 (V-[ n ]-T-Alg-rec X p) s = refl

-- The recursor is unique as a function
V-[_]-T-rec-unique : (n : ℕ)
                   → {i j : Level}
                   → (X : T-[ n ]-Alg i j)
                   → (p : is-[ succ-ℕ n ]-small i ¦ X ¦)
                   → (φ : hom-T-[ n ]-Alg (V-T-[ n ]-Alg i) X p)
                   → pr1 φ ~ V-[ n ]-T-rec ¦ X ¦ p (X ↓)
V-[ n ]-T-rec-unique X p φ =
  V-[ n ]-elim
    (λ x → φ 〈 x 〉 == V-[ n ]-T-rec ¦ X ¦ p (X ↓) x)
    (λ A f IH →
      pr2 φ (A , f) ∙
      ap (λ h →
            (X ↓)
            (trunc-Image p h ,
             trunc-image-inclusion p h))
         (eq-htpy IH))

-- The recursor is unique as a Tⁿ-Alg homomorphism
V-[_]-T-Alg-Eq-rec-unique : (n : ℕ)
                          → {i j : Level}
                          → (X : T-[ n ]-Alg i j)
                          → (p : is-[ succ-ℕ n ]-small i ¦ X ¦)
                          → (φ : hom-T-[ n ]-Alg (V-T-[ n ]-Alg i) X p)
                          → hom-T-[ n ]-Alg-Eq (V-T-[ n ]-Alg i) X p φ (V-[ n ]-T-Alg-rec X p)
pr1 (V-[ n ]-T-Alg-Eq-rec-unique X p φ) = V-[ n ]-T-rec-unique X p φ
pr2 (V-[ n ]-T-Alg-Eq-rec-unique X p (φ , α)) (A , f) =
  ap (λ q → α (A , f) ∙ ap (X ↓) q)
      (ap-comp _
         (_∘ map-trunc-map f)
         (eq-htpy (V-[ n ]-T-rec-unique X p (φ , α)))) ∙
  (ap (λ q → α (A , f) ∙
              ap (X ↓) (ap (λ h → trunc-Image p h , trunc-image-inclusion p h) q))
       (eq-htpy-comp (map-trunc-map f) (V-[ n ]-T-rec-unique X p (φ , α))) ∙
  (ap (α (A , f) ∙_) (inv (ap-comp (X ↓) _ _)) ∙
  (inv (V-[ n ]-elim-comp
         (λ x → φ x == V-[ n ]-T-rec ¦ X ¦ p (X ↓) x)
         (λ A f IH →
           α (A , f) ∙
           ap (λ h → (X ↓) (trunc-Image p h , trunc-image-inclusion p h)) (eq-htpy IH))
         A f) ∙
  inv right-unit)))

V-[_]-T-Alg-rec-unique : (n : ℕ)
                       → {i j : Level}
                       → (X : T-[ n ]-Alg i j)
                       → (p : is-[ succ-ℕ n ]-small i ¦ X ¦)
                       → (φ : hom-T-[ n ]-Alg (V-T-[ n ]-Alg i) X p)
                       → φ == V-[ n ]-T-Alg-rec X p
V-[ n ]-T-Alg-rec-unique X p φ =
  hom-T-[ n ]-Alg-eq {Y = X} p φ (V-[ n ]-T-Alg-rec X p) (V-[ n ]-T-Alg-Eq-rec-unique X p φ)

{- Cumulativity of Vⁿ -}

map-V∞-V∞⁺ : ∀ i → V∞ i → V∞ (lsuc i)
map-V∞-V∞⁺ i (sup A f) = sup (raise (lsuc i) A) (λ a → map-V∞-V∞⁺ i (f (map-inv-raise a)))

V∞-in-V∞⁺ : ∀ i → V∞ (lsuc i)
V∞-in-V∞⁺ i = sup (V∞ i) (map-V∞-V∞⁺ i)

is-emb-map-V∞-V∞⁺ : ∀ {i} → is-emb (map-V∞-V∞⁺ i)
is-emb-map-V∞-V∞⁺ {i} (sup A f) (sup B g) =
  is-equiv-equiv'
    {f =
      ap (map-Σ
           (λ A → A → V∞ (lsuc i))
           (raise (lsuc i))
           (λ A f a → map-V∞-V∞⁺ i (f (map-inv-raise a))))}
    (equiv-ap equiv-structure-𝕎-Alg (A , f) (B , g))
    (equiv-ap equiv-structure-𝕎-Alg _ _)
    (λ { refl → refl })
    (is-equiv-htpy
      (ap (tot (λ A' f' → map-V∞-V∞⁺ i ∘ f')) ∘
       ap (map-Σ (λ A → A → V∞ i) (raise (lsuc i)) (λ A f a → f (map-inv-raise a))))
      (λ { refl → refl })
      (is-equiv-comp
        (ap (tot (λ A' f' → map-V∞-V∞⁺ i ∘ f')))
        (ap (map-Σ (λ A → A → V∞ i) (raise (lsuc i)) (λ A f a → f (map-inv-raise a))))
        (is-emb-map-Σ _
          (is-emb-raise (lsuc i))
          (λ A' →
            is-emb-is-equiv
              (is-equiv-map-equiv
                (equiv-precomp-Π
                  (inv-equiv (compute-raise (lsuc i) A'))
                  (λ _ → V∞ i))))
          (A , f)
          (B , g))
        (is-equiv-equiv
          (equiv-eq-T∞
            (raise (lsuc i) A , f ∘ map-inv-raise)
            (raise (lsuc i) B , g ∘ map-inv-raise))
          (equiv-eq-T∞
            (raise (lsuc i) A , map-V∞-V∞⁺ i ∘ f ∘ map-inv-raise)
            (raise (lsuc i) B , map-V∞-V∞⁺ i ∘ g ∘ map-inv-raise))
          lem1
          (is-equiv-tot-is-fiberwise-equiv (λ e →
            is-equiv-map-Π-is-fiberwise-equiv (λ a →
              is-emb-map-V∞-V∞⁺
                (f (map-inv-raise a))
                (g (map-inv-raise (map-equiv e a)))))))))
  where
    lem1 : {(A' , f') (B' , g') : T∞ (lsuc i) (V∞ i)}
         → map-equiv (equiv-eq-T∞ (A' , map-V∞-V∞⁺ i ∘ f') (B' , map-V∞-V∞⁺ i ∘ g'))
           ∘ ap (tot (λ A'' f'' → map-V∞-V∞⁺ i ∘ f''))
         ~ tot (λ e H a → ap (map-V∞-V∞⁺ i) (H a))
           ∘ map-equiv (equiv-eq-T∞ (A' , f') (B' , g'))
    lem1 refl = refl

V∞↪V∞⁺ : ∀ i → V∞ i ↪ V∞ (lsuc i)
pr1 (V∞↪V∞⁺ i) = map-V∞-V∞⁺ i
pr2 (V∞↪V∞⁺ i) = is-emb-map-V∞-V∞⁺

is-[_]-iterative-set-V∞-V∞⁺ : ∀ {i} (n : 𝕋) (x : V∞ i)
                            → is-[ succ-𝕋 n ]-iterative-set x
                            → is-[ succ-𝕋 n ]-iterative-set (map-V∞-V∞⁺ i x)
pr1 (is-[_]-iterative-set-V∞-V∞⁺ {i} n (sup A f) (p , q)) =
  is-trunc-map-comp (succ-𝕋 n)
    (map-V∞-V∞⁺ i ∘ f)
    map-inv-raise
    (is-trunc-map-comp (succ-𝕋 n)
      (map-V∞-V∞⁺ i)
      f
      (is-trunc-map-is-prop-map n
        (is-prop-map-is-emb is-emb-map-V∞-V∞⁺))
      p)
    (is-trunc-map-is-equiv (succ-𝕋 n)
      (is-equiv-map-inv-equiv (compute-raise _ A)))
pr2 (is-[ n ]-iterative-set-V∞-V∞⁺ (sup A f) (p , q)) (map-raise a) =
  is-[ n ]-iterative-set-V∞-V∞⁺ (f a) (q a)

V-[_]↪V⁺ : (n : ℕ) (i : Level) → V-[ n ] i ↪ V-[ n ] (lsuc i)
V-[ n ]↪V⁺ i =
  emb-into-subtype
    is-[ minus-one n ]-iterative-set-Prop
    (comp-emb (V∞↪V∞⁺ i) V-[ n ]↪V∞)
    (λ (x , p) → is-[ minus-two n ]-iterative-set-V∞-V∞⁺ x p)

V-[_]-in-V⁺ : (n : ℕ) (i : Level) → V-[ n ] (lsuc i)
V-[ n ]-in-V⁺ i =
  sup-[ n ]
    (V-[ n ] i ,
    pr1 (V-[ n ]↪V⁺ i) ,
    is-trunc-map-is-prop-map (minus-two n) (is-prop-map-is-emb (pr2 (V-[ n ]↪V⁺ i))))

{- W-types in Vⁿ -}

W∞ : ∀ {i} (ordered-pairs : V∞ i × V∞ i ↪ V∞ i)
   → (A : V∞ i) → (El∞ A → V∞ i) → V∞ i
W∞ {i} ordered-pairs A B = sup (W A' B') map-W-A-B
  where
    import e-structure.core
    open e-structure.core.ordered-pairing-structure.notation (V∞ i) ordered-pairs

    A' : UU i
    A' = El∞ A

    B' : A' → UU i
    B' = El∞ ∘ B

    f : A' → (V∞ i)
    f = pr2 (desup∞ A)

    g : ∀ a → B' a → V∞ i
    g a = pr2 (desup∞ (B a))

    map-W-A-B : W A' B' → V∞ i
    map-W-A-B (sup a α) = ⟨ f a , sup (B' a) (λ b → ⟨ g a b , map-W-A-B (α b) ⟩) ⟩

{- V⁰ as a universe -}

module _ {i : Level} where
  open import e-structure.from-T-n-coalgebra
    (zero-ℕ)
    (V⁰-T⁰-Coalg i)
    (is-emb-is-equiv (pr2 desup⁰-equiv))

  is-set-El⁰ : (x : V⁰ i) → is-set (El⁰ x)
  is-set-El⁰ = is-trunc-index-type

  is-set-V⁰ : is-set (V⁰ i)
  is-set-V⁰ = is-trunc-carrier-T-Coalg

V⁰-Set : ∀ i → Set (lsuc i)
pr1 (V⁰-Set i) = V⁰ i
pr2 (V⁰-Set i) = is-set-V⁰

El⁰-Set : ∀ i → V⁰ i → Set i
pr1 (El⁰-Set i x) = El⁰ x
pr2 (El⁰-Set i x) = is-set-El⁰ x

module _ {i : Level} where

  empty⁰ : V⁰ i
  empty⁰ = sup⁰' (raise-empty i , raise-ex-falso-emb i)

  unit⁰ : V⁰ i
  unit⁰ =
    sup⁰' (raise-unit i ,
          (λ s → empty⁰) ,
          is-emb-is-prop-is-set is-prop-raise-unit is-set-V⁰)

  empty⁰≠unit⁰ : empty⁰ ≠ unit⁰
  empty⁰≠unit⁰ empty⁰=unit⁰ =
    map-inv-raise
      (map-inv-equiv
        (pr1 (map-equiv (equiv-eq-Eq-V empty⁰ unit⁰) empty⁰=unit⁰))
        (map-raise star))

  bool⁰ : V⁰ i
  bool⁰ = sup⁰' (raise-bool i , ι-emb)
    where
      ι : raise-bool i → V⁰ i
      ι (map-raise true) = unit⁰
      ι (map-raise false) = empty⁰

      is-inj-ι : {x y : raise-bool i} → ι x == ι y → x == y
      is-inj-ι {map-raise false} {map-raise false} eq = refl
      is-inj-ι {map-raise true} {map-raise true} eq = refl
      is-inj-ι {map-raise true} {map-raise false} eq = raise-ex-falso i (tr El⁰ eq (map-raise star))
      is-inj-ι {map-raise false} {map-raise true} eq = raise-ex-falso i (tr El⁰ (inv eq) (map-raise star))

      ι-emb : raise-bool i ↪ V⁰ i
      pr1 ι-emb = ι
      pr2 ι-emb = is-emb-is-injective is-set-V⁰ is-inj-ι



module _ {i : Level} where
  open import fixed-point.unordered-tupling
    0 0 0 refl (V⁰ i) (desup⁰-equiv) is-locally-small-V
  open ordered-pairs-from-k=0 refl
  open import fixed-point.exponentiation
    0 (V⁰ i) (desup⁰-equiv) ordered-pairs

  Π⁰ : (A : V⁰ i) → (El⁰ A → V⁰ i) → V⁰ i
  Π⁰ A B = sup⁰ ((∀ a → B' a) , graph f g , is-trunc-map-graph f g) where
      A' : UU i
      A' = El⁰ A

      B' : A' → UU i
      B' = El⁰ ∘ B

      f : prop-map A' (V⁰ i)
      f = pr2 (desup⁰ A)

      g : ∀ a → prop-map (B' a) (V⁰ i)
      g a = pr2 (desup⁰ (B a))

  Σ⁰ : (A : V⁰ i) → (El⁰ A → V⁰ i) → V⁰ i
  Σ⁰ A B = sup⁰ (Σ A' B' , comp-prop-map
                             (prop-map-emb ordered-pairs)
                             ((map-Σ _ (f 〈_〉) (_〈_〉 ∘ g)) , is-prop-map-map-Σ _ (pr2 f) (pr2 ∘ g)))
    where
      A' : UU i
      A' = El⁰ A

      B' : A' → UU i
      B' = El⁰ ∘ B

      f : prop-map A' (V⁰ i)
      f = pr2 (desup⁰ A)

      g : ∀ a → prop-map (B' a) (V⁰ i)
      g a = pr2 (desup⁰ (B a))

  _→⁰_ : V⁰ i → V⁰ i → V⁰ i
  A →⁰ B = Π⁰ A (λ _ → B)

  _×⁰_ : V⁰ i → V⁰ i → V⁰ i
  A ×⁰ B = Σ⁰ A (λ _ → B)

  _+⁰_ : V⁰ i → V⁰ i → V⁰ i
  A +⁰ B = sup⁰ (El⁰ A + El⁰ B , prop-map-f-g)
    where
      f : El⁰ A ↪ V⁰ i
      f = emb-prop-map
            (comp-prop-map
              ((λ x → ⟨ empty⁰ , x ⟩) ,
               is-prop-map-fix-pr1
                 (is-prop-map-is-emb (pr2 ordered-pairs))
                 is-set-V⁰
                 empty⁰)
              (pr2 (desup⁰ A)))

      g : El⁰ B ↪ V⁰ i
      g = emb-prop-map
            (comp-prop-map
              ((λ x → ⟨ unit⁰ , x ⟩) ,
               is-prop-map-fix-pr1
                 (is-prop-map-is-emb (pr2 ordered-pairs))
                 is-set-V⁰
                 unit⁰)
              (pr2 (desup⁰ B)))

      no-overlap : (a : El⁰ A) (b : El⁰ B) → f 〈 a 〉 ≠ g 〈 b 〉
      no-overlap a b fa=gb =
        empty⁰≠unit⁰
          (ap pr1
              (map-inv-is-equiv
                (pr2 ordered-pairs
                  (empty⁰ , pr2 (desup⁰ A) 〈 a 〉)
                  (unit⁰ , pr2 (desup⁰ B) 〈 b 〉))
                fa=gb))

      prop-map-f-g : prop-map (El⁰ A + El⁰ B) (V⁰ i)
      pr1 prop-map-f-g = ind-coprod _ (pr1 f) (pr1 g)
      pr2 prop-map-f-g = is-prop-map-is-emb (is-emb-coprod (pr2 f) (pr2 g) no-overlap)

  open import fixed-point.natural-numbers 0 (V⁰ i) (desup⁰-equiv)

  ℕ⁰ : V⁰ i
  ℕ⁰ = pr1 (natural-numbers-von-neumann is-locally-small-V⁰)

  Id⁰ : (A : V⁰ i) → El⁰ A → El⁰ A → V⁰ i
  Id⁰ A a a' =
    sup⁰' (a == a' ,
          (λ _ → empty⁰) ,
          is-emb-is-prop-is-set (is-set-El⁰ A a a') is-set-V⁰)

  fiber⁰ : (A B : V⁰ i) → (El⁰ A → El⁰ B) → El⁰ B → V⁰ i
  fiber⁰ A B f b = Σ⁰ A (λ a → Id⁰ B (f a) b)

  fiber'⁰ : (A B : V⁰ i) → (El⁰ A → El⁰ B) → El⁰ B → V⁰ i
  fiber'⁰ A B f b = Σ⁰ A (λ a → Id⁰ B b (f a))

  equiv-class : (A : V⁰ i) (R : El⁰ A → El⁰ A → Prop i) 
              → El⁰ A → V⁰ i
  equiv-class A R a = sup⁰ (type-subtype (R a)
                           , comp-prop-map (pr2 (desup⁰ A))
                                           (prop-map-subtype (R a)))


  equiv-class-≃
              : (A : V⁰ i)(R : El⁰ A → El⁰ A → Prop i)
              → (∀ a a' → (∀ b → ¦ R a b ¦ ≃ ¦ R a' b ¦ ) ≃ ¦ R a a' ¦)
              → ∀ a a' → (equiv-class A R a == equiv-class A R a')
                       ≃ ¦ R a a' ¦
  equiv-class-≃ A R P a a'
              = equivalence-reasoning
                     equiv-class A R a == equiv-class A R a'
                       ≃  Σ (Σ _ (¦R¦ a) ≃ Σ _ (¦R¦ a'))
                            (λ α → ∀ x → V⁰↪V∞ 〈 f 〈 pr1 x 〉 〉 ==V∞ V⁰↪V∞ 〈 f 〈 pr1 (α 〈 x 〉)〉 〉)
                                by equiv-eq-Eq-V _ _
                       ≃  (Σ (Σ _ (¦R¦ a) ≃ Σ _ (¦R¦ a')) λ α → ∀ x → pr1 x == pr1 (α 〈 x 〉))
                                by equiv-tot (λ α → equivalence-reasoning
                                                (∀ x → V⁰↪V∞ 〈 f 〈 pr1 x 〉 〉 ==V∞ V⁰↪V∞ 〈 f 〈 pr1 (α 〈 x 〉)〉 〉)
                                              ≃ (∀ x → V⁰↪V∞ 〈 f 〈 pr1 x 〉 〉 == V⁰↪V∞ 〈 f 〈 pr1 (α 〈 x 〉)〉 〉)
                                                      by equiv-Π-equiv-family (λ x → (equiv-eq-V∞ _ _)⁻¹)
                                              ≃ (∀ x → f 〈 pr1 x 〉 == f 〈 pr1 (α 〈 x 〉)〉)
                                                      by equiv-Π-equiv-family (λ x → equiv-ap-emb V⁰↪V∞ ⁻¹)
                                              ≃ (∀ x → pr1 x == pr1 (α 〈 x 〉))
                                                      by equiv-htpy-postcomp-is-emb (emb-prop-map f) _ _ ⁻¹)
                       ≃  (∀ b → ¦ R a b ¦ ≃ ¦ R a' b ¦)
                               by equiv-fam-equiv-equiv-tot-space _ _ ⁻¹
                       ≃  ¦ R a a' ¦
                               by P a a' where
                          f : prop-map (El⁰ A ) (V⁰ i)
                          f = pr2 (desup⁰ A)
                          ¦R¦ : El⁰ A → El⁰ A → UU i
                          ¦R¦ a b = ¦ R a b ¦

  equiv-class' : (A : V⁰ i) (R : El⁰ A → El⁰ A → UU i) 
              → El⁰ A → V⁰ i
  equiv-class' A R a = equiv-class A ∥ R ∥ a

  _/⁰_ : (A : V⁰ i) (R : El⁰ A → El⁰ A → UU i) → V⁰ i
  A /⁰ R = sup⁰ (set-quotient R , ( f
                                , is-prop-map-is-emb (is-emb-is-injective (is-set-V⁰)
                                                                          (λ {a₀} {a₁} → injective-f a₀ a₁)))) where
             f : set-quotient R → V⁰ i
             f = set-quotient-rec (R)
                                  (is-set-V⁰)
                                  (equiv-class A ∥ R ∥)
                                  (λ {a₀} {a₁} → (equiv-class-≃ A ∥ R ∥ (λ a a' → ∥ R ∥-equivalence-class-representation _ _) a₀ a₁ ⁻¹) 〈_〉 ∘ quot-rel)
             injective-f : ∀ a₀ a₁ → f a₀ == f a₁ → a₀ == a₁
             injective-f a₀ a₁ = set-quotient-prop-elim (R)
                                                        {P = λ a₀ → ∀ a₁ → f a₀ == f a₁ → a₀ == a₁}
                                                        (λ _ → is-prop-Π (λ _ → is-prop-function-type (set-quotient-is-set _ _)))
                                                        (λ a₀' → set-quotient-prop-elim (R)
                                                                                        {P = λ a₁ → _ → q[ a₀' ] == a₁}
                                                                                        (λ _ → is-prop-function-type (set-quotient-is-set _ _))
                                                        (λ a₁' → equiv-class-≃ A ∥ R ∥ (λ a a' → ∥ R ∥-equivalence-class-representation _ _) a₀' a₁' 〈_〉)) a₀ a₁