{-# OPTIONS --cubical #-}

open import Cubical.Core.Everything

postulate
  magic : ∀ {i} {X : Set i} → X

test : Type₁
test = Type ℓ-zero

Type₂ = Type (ℓ-suc (ℓ-suc ℓ-zero))

-- \ell
Type' : (ℓ : Level) → Set (ℓ-suc ℓ)
Type' ℓ = Set ℓ

test₂ : Type₂
test₂ = Type₁

variable
  ℓ ℓ' : Level
  A : Type ℓ

refl : ∀ {x : A} → x ≡ x
refl {x = x} = λ i → x

apd : ∀ (C : A → Type ℓ') (f : (x : A) → C x) {x y : A} (p : x ≡ y)
  → (λ i → C (p i)) [ f x ≡ f y ]
apd C f p = λ i → f (p i)

funext : ∀ (B : A → Type ℓ') (f g : (x : A) → B x)
  → ((x : A) → f x ≡ g x) → f ≡ g
funext B f g hmtp i x = hmtp x i

≡Σ : ∀ {A : Type ℓ} {B : A → Type ℓ'} (x y : Σ A B) → Type (ℓ-max ℓ ℓ')
≡Σ {B = B} x y = Σ (fst x ≡ fst y) (λ ≡a → (λ i → B (≡a i)) [ snd x ≡ snd y ])

postulate
  equiv : ∀ {B : Type ℓ'}
    → (f : A → B) (g : B → A) (f-g : (y : B) → f (g y) ≡ y) (g-f : (x : A) → g (f x) ≡ x)
    → A ≃ B

≡Σ-econv : ∀ {B : A → Type ℓ'} (x y : Σ A B) → (x ≡ y) ≃ (≡Σ x y)
≡Σ-econv x y = equiv f g f-g g-f where
  f : x ≡ y → ≡Σ x y
  f p = (λ i → fst (p i)) , (λ i → snd (p i))

  g : ≡Σ x y → x ≡ y
  g (p , q) = λ i → p i , q i

  f-g : ∀ x → f (g x) ≡ x
  f-g _ = refl

  g-f : ∀ x → g (f x) ≡ x
  g-f _ = refl