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

open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.propositional-maps
open import foundation.sets
open import foundation.truncated-maps
open import foundation.truncated-types
open import foundation.truncation-levels
  renaming (truncation-level-minus-one-ℕ to minus-one;
    truncation-level-ℕ to to-𝕋)

open import e-structure.core
open import functor.n-slice
open import notation

module e-structure.from-T-n-coalgebra
  {i j} (n : ℕ) (X : T-[ n ]-Coalg i j) (p : is-emb (X ↓)) where

is-emb-to-T∞ : is-emb (pr2 (T-[ n ]-to-T∞-Coalg X))
is-emb-to-T∞ =
  is-emb-comp
    (map-emb (emb-forget-T-[ n ]-to-T∞ ¦ X ¦))
    (X ↓)
    (is-emb-map-emb (emb-forget-T-[ n ]-to-T∞ ¦ X ¦))
    (p)

open import e-structure.from-T-coalgebra (T-[ n ]-to-T∞-Coalg X) is-emb-to-T∞
  renaming (is-extensional-T∞ to is-extensional-T; ∈-structure-T∞ to ∈-structure-T) public

-- The ∈-relation has h-level n-1
is-trunc-∈ : {x y : ¦ X ¦} → is-trunc (minus-one n) (y ∈ x)
is-trunc-∈ {x} {y} = pr2 (pr2 ((X ↓) x)) y

-- The carrier has h-level n
is-trunc-carrier-T-Coalg : is-trunc (to-𝕋 n) ¦ X ¦
is-trunc-carrier-T-Coalg x y =
  is-trunc-equiv (minus-one n) _
    equiv-extensionality
    (is-trunc-Π _ (λ _ →
      is-trunc-equiv-is-trunc _
        is-trunc-∈
        is-trunc-∈))

-- The index type of any element in the carrier has h-level n
is-trunc-index-type : (x : ¦ X ¦) → is-trunc (to-𝕋 n) ¦ (X ↓) x ¦
is-trunc-index-type x =
  is-trunc-equiv (to-𝕋 n) _
    (inv-equiv-total-fiber (map-trunc-map (pr2 ((X ↓) x))))
    (is-trunc-Σ
      is-trunc-carrier-T-Coalg
      (λ x → is-trunc-succ-is-trunc (minus-one n) is-trunc-∈))