{-# OPTIONS --safe #-}

module Prelude where

open import Data.Sigma public
open import Data.Empty public
open import Data.Unit public
open import Data.Bool public
open import Data.Nat public
open import Data.Maybe public
open import Level public
-- open import Level.Literals public
open import Function public
open import Path public
open import Data.Sum public
open import Isomorphism public
open import Data.List public
open import HLevels public
open import Decidable public
open import Discrete public
open import Discrete.IsSet public
open import Agda.Builtin.FromNat public
open import Path.Reasoning public

open import Data.Unit.UniversePolymorphic
  renaming (⊤ to Poly-⊤; tt to Poly-tt)
  public

open import Data.Empty.UniversePolymorphic
  renaming (⊥ to Poly-⊥; absurd to Poly-absurd)
  public
open import Data.Empty.Properties
  using (isProp⊥)
  public

-- open import HITs.SetQuotients public
-- open import HITs.PropositionalTruncation public

-- open import Data.Sigma.Properties public

-- open import WellFounded public
-- open import Path.Reasoning public

it : ⦃ inst : A ⦄ → A
it ⦃ inst ⦄ = inst