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


open import foundation-core.truncated-types
open import foundation-core.truncation-levels
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.universe-levels


module notation where

¦_¦ : ∀ {i j} {B : UU i → UU j} → Σ (UU i) B → UU i
¦_¦ = pr1


infix  _〈_〉

_〈_〉 : ∀ {i j k} {A : UU i} {B : A → UU j} {C : ((a : A) → B a) → UU k}
    → Σ ((a : A) → B a) C
    → (a : A) → B a
f 〈 a 〉 = pr1 f a

infix  _↓

_↓ : ∀ {i j} {B : UU i → UU j}
   → (x : Σ (UU i) B) → B ¦ x ¦
_↓ = pr2 

infix  _==_

_==_ : ∀ {i} {A : UU i} → A → A → UU i
x == y = Id x y

open import trees.w-types renaming (Eq-𝕎 to _==W_) public

W : ∀ {i j} (A : UU i) (B : A → UU j) → UU (i ⊔ j)
W = 𝕎

pattern sup A f = tree-𝕎 A f


open 𝕋 renaming (neg-two-𝕋 to neg-two-T ; succ-𝕋 to succ-T)

TLevel = 𝕋

neg-one-T = neg-one-𝕋
zero-T = zero-𝕋

infix  _⁻¹

_⁻¹ : ∀ {i j} {A : UU i}{B : UU j}
    → A ≃ B → B ≃ A
e ⁻¹ = inv-equiv e