{-# OPTIONS --cubical --exact-split #-} -- not safe

module Cubical.Structures.Prelude.TODO where

open import Agda.Primitive
open import Cubical.Foundations.Prelude

postulate
  TODO : {a : Level} {A : Type a} -> A