{-# OPTIONS --safe #-}
module Cubical.Data.Empty.Base where

open import Cubical.Foundations.Prelude

private
  variable
     ℓ' : Level

data  : Type₀ where

⊥* : Type 
⊥* = Lift 

rec : {A : Type }    A
rec ()

rec* : {A : Type }  ⊥* { = ℓ'}  A
rec* ()

elim : {A :   Type }  (x : )  A x
elim ()

elim* : {A : ⊥* {ℓ'}  Type }  (x : ⊥* {ℓ'})  A x
elim* ()