module Base where

-- Precedence -------------------------------------

infixr 1  _⊎_
infixr 2  _×_ _,_

-- Basic Datatypes --------------------------------------------------------------

data False : Set where

data Unit : Set where
  unit : Unit

data Bool : Set where
  false : Bool
  true  : Bool

{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  true  #-}
{-# BUILTIN FALSE false #-}

data Maybe (A : Set) : Set where
  nothing : Maybe A
  just    : A  Maybe A

-- Dependent Products (Σ types)

record Σ (A : Set) (B : A  Set) : Set where
  constructor _,_
  field
    fst : A
    snd : B fst

open Σ public

-- data Σ (A : Set) (B : A → Set) : Set where
--   _,_ : (a : A) → B a → Σ A B

syntax Σ A  a  B) = Σ[ a ∶ A ] B

-- Cartesian Product

_×_ : Set  Set  Set
A × B = Σ A  _  B)

-- Sum Types (a.k.a. co-products) --

data _⊎_ (A B : Set) : Set where
  inl : A  A  B
  inr : B  A  B

-- Binary Operators

Op : Set  Set
Op A = A  A  A