Basics.agda

module Basics where

_%_ : {A B : Set}{C : B -> Set}
      (f : (x : B) -> C x)(g : A -> B)(x : A) -> C (g x)
f % g = \x -> f (g x)

-- Logic

data   False : Set where
record True  : Set where

tt : True
tt = _

¬_ : Set -> Set
¬ A = A -> False

record ∃ {A : Set}(P : A -> Set) : Set where
  field
    witness : A
    proof   : P witness

∃-intro : {A : Set}{P : A -> Set}(x : A) -> P x -> ∃ P
∃-intro x p = record { witness = x; proof = p }

infixr 15 _/\_ _×_

data _×_ (A B : Set) : Set where
  _,_ : A -> B -> A × B

_/\_ = _×_

-- Maybe

data Lift (A : Set) : Set where
  bot  : Lift A
  lift : A -> Lift A

_=<<_ : {A B : Set} -> (A -> Lift B) -> Lift A -> Lift B
f =<< bot    = bot
f =<< lift v = f v

-- Nat

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

-- Identity

infix 10 _==_

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

data Id {A : Set}(x : A) : Set where
  it : (y : A) -> x == y -> Id x

-- Booleans

data Bool : Set where
  true  : Bool
  false : Bool

data LR : Set where
  left  : LR
  right : LR

if_then_else_ : {A : Set} -> Bool -> A -> A -> A
if true  then x else y = x
if false then x else y = y

-- Lists

infixr 50 _::_

data List (A : Set) : Set where
  []   : List A
  _::_ : A -> List A -> List A

data Elem {A : Set}(x : A) : List A -> Set where
  hd : forall {xs} -> Elem x (x :: xs)
  tl : forall {y xs} -> Elem x xs -> Elem x (y :: xs)