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

open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.empty-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.functoriality-dependent-pair-types
open import foundation.propositional-maps
open import foundation.truncated-maps
open import foundation.type-arithmetic-empty-type
open import foundation.universe-levels
open import foundation.univalence

open import order-theory.well-founded-orders

open import functor.n-slice
open import notation hiding (sup)

module fixed-point.empty-set {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 unordered tupling
open import e-structure.property.unordered-tupling ∈-structure-V

∅ : V
∅ = sup (raise-empty i ,
        raise-ex-falso i ,
        is-trunc-map-is-prop-map _
          (is-prop-map-is-emb
            (is-emb-map-emb (raise-ex-falso-emb i))))

-- We can construct the empty set
empty-set : EmptySet
pr1 empty-set = ∅
pr2 empty-set x =
  equivalence-reasoning
    x ∈ ∅
      ≃ fiber (raise-ex-falso i) x        by equiv-eq (∈-sup x)
      ≃ Σ empty (λ s → ex-falso s == x) by equiv-Σ-equiv-base
                                             (λ s → ex-falso s == x)
                                             (inv-equiv (compute-raise-empty i))
      ≃ empty                           by left-absorption-Σ (λ s → ex-falso s == x)

open empty-set.properties empty-set public