module Base where

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

infixr   _⊎_
infixr   _×_ _,_

-- 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