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

module Pi.Common.Extra where

postulate
  TODO! : ∀ {i} {A : Set i} → A
  TODO- : ∀ {i} {A : Set i} → A
  TODO : ∀ {i} {A : Set i} → A