{-# 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 ()