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

module DepthComonads.Empty where

open import DepthComonads.Level

data ⊥ : Type where

infix 4.5 ¬_
¬_ : Type a → Type a
¬ A = A → ⊥

⊥-elim : ⊥ → A
⊥-elim ()