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

open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.existential-quantification
open import foundation.truncations
open import foundation.truncation-levels
  renaming (truncation-level-minus-one-ℕ to minus-one)
open import foundation.universe-levels

open import e-structure.core
open import notation

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

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

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

-- Special case
0-Replacement : UU (i ⊔ j)
0-Replacement = [ zero-ℕ ]-Replacement

∞-Replacement : UU (i ⊔ j)
∞-Replacement = (a : M) → (f : El a → M)
  → Σ M (λ [fa] → (z : M) → (z ∈ [fa]) ≃ Σ (El a) λ (x , p) → f (x , p) == z)