module Cubical.Structures.Prelude.TODO where

open import Cubical.Structures.Prelude

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