{-# OPTIONS --safe --cubical #-}

module Prelude where

open import Level public
open import Data.Sigma public
open import Function.Fiber public
open import Data.Empty public
open import Data.Unit public
open import Data.Nat public
  using (ℕ; suc; zero)
open import Data.Bool public
  using (Bool; true; false; bool; if_then_else_; T; _and_; _or_; not)
open import Data.Maybe public
  using (Maybe; just; nothing)
open import HITs.PropositionalTruncation public
  using (∥_∥; ∣_∣)
open import Function.Surjective public
  using (Surjective; SplitSurjective; _↠!_; _↠_)
open import Data.Pi public
open import Function.Isomorphism public
open import Path public
open import Function public
open import Relation.Nullary.Decidable public
open import Relation.Nullary.Discrete public using (Discrete)
open import Relation.Nullary.Discrete.Properties public using (Discrete→isSet)
open import HLevels public
open import Data.Sum public
open import Equiv public
open import Data.Lift public
open import Function.Biconditional public
open import Relation.Unary public
open import Strict public
open import Instance public