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

open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.identity-types
open import foundation.truncated-maps
open import foundation.truncated-types
open import foundation.truncation-levels
  renaming (truncation-level-ℕ to to-𝕋)
open import foundation.universe-levels

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

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

sup : T-[ n ] i V → V
sup = map-inv-equiv fixed-point-V

desup : V → T-[ n ] i V
desup = map-equiv fixed-point-V

is-equiv-desup : is-equiv desup
is-equiv-desup = is-equiv-map-equiv fixed-point-V

is-emb-desup : is-emb desup
is-emb-desup = is-emb-is-equiv is-equiv-desup

open import e-structure.from-T-n-coalgebra n (V , desup) is-emb-desup public
  renaming (is-extensional-T to is-extensional-V; is-trunc-carrier-T-Coalg to is-trunc-V;
           ∈-structure-T to ∈-structure-V)

-- Proof that V is n-truncated using the fact that
-- it is a fixedpoint for Tⁿ
is-trunc-V' : is-trunc (to-𝕋 n) V
is-trunc-V' = is-trunc-equiv _ _ fixed-point-V is-trunc-T-[ n ]

∈-sup : ∀ {A f}
      → (x : V)
      → (x ∈ sup (A , f)) == (Σ A (λ a → map-trunc-map f a == x))
∈-sup {A} {f} x =
  ap (λ (B , g) → Σ B (λ b → map-trunc-map g b == x))
     (is-section-map-inv-equiv fixed-point-V (A , f))