{-# OPTIONS --cubical-compatible #-}
module Terra.Data.Counit where
open import Terra.Data.Level
private
  variable
    ℓ : Level

data ⊥ : Set where
  -- rien

⊥-elim : {T : Set ℓ} -> ⊥ -> T
⊥-elim ()

absurd : {A : Set ℓ} -> ⊥ -> A
absurd ()