{- Basic definitions and lemmas. -} module basic where open import basic.prelude public open import basic.coproduct public open import basic.empty public open import basic.equality public open import basic.flat public open import basic.function public open import basic.isomorphism public open import basic.natural-number public open import basic.retract public open import basic.sigma public open import basic.unit public