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

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-extensionality
open import foundation.functoriality-dependent-pair-types
open import foundation.identity-types
open import foundation.raising-universe-levels
open import foundation.slice
open import foundation.subtypes
open import foundation.transport-along-identifications
open import foundation.univalence
open import foundation.universe-levels

open import e-structure.core
open import e-structure.u-like
open import functor.slice
open import notation

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

U-like-∈-structure-T∞ : Σ (¦ X ¦ → ¦ X ¦ → UU (i ⊔ j))
                       (λ _∈_ → (i -like (¦ X ¦ , _∈_)) × is-extensional _∈_)
U-like-∈-structure-T∞ =
  map-equiv
    (equiv-T∞-Coalg-emb-∈-structure ¦ X ¦ i)
    (X ↓ , p)

_∈_ : ¦ X ¦ → ¦ X ¦ → UU (i ⊔ j)
x ∈ y = let (A , f) = (X ↓) y in fiber f x

is-extensional-T∞ : is-extensional _∈_
is-extensional-T∞ =
  tr is-extensional
     (eq-htpy (λ x →
       eq-htpy (λ y →
         eq-equiv _ _
           (equiv-Σ-equiv-base _
             (inv-equiv (compute-raise (i ⊔ j) (pr1 ((X ↓) y))))))))
     (pr2 (pr2 U-like-∈-structure-T∞))

∈-structure-T∞ : ∈-structure j (i ⊔ j)
∈-structure-T∞ = ((¦ X ¦ , _∈_) , is-extensional-T∞)

-- Import extensionality equivalence
open e-structure.core.extensionality ∈-structure-T∞ public
-- Import the notation El
open e-structure.core.elements (¦ X ¦ , _∈_) public