module Prelude.Basic where

-- Basic types re-exported from the standard library

open import Function          public

open import Data.Product      public
open import Data.Sum renaming (map to ⊎-map) public

open import Agda.Builtin.Unit public -- fewer names clashes than Data.Unit
open import Data.Bool renaming (_≟_ to _𝔹≟_; T to Oh) public
open import Data.Nat renaming (_⊔_ to _ℕ⊔_)           public

open import Level renaming (zero to lzero; suc to lsuc) public

-- universe polymorphic empty type
data ⊥ {a : Level} : Set a where

⊥-elim : ∀ {a w} {Whatever : Set w} → ⊥ {a} → Whatever
⊥-elim ()

-- Notation for Pi-types

∏ : (S : Set)(T : S -> Set1) -> Set1
∏ S T = (s : S) -> T s