Prelude.agda

module Prelude where

id : {A : Set} -> A -> A
id x = x

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

flip : {A B C : Set} -> (A -> B -> C) -> B -> A -> C
flip f x y = f y x

Rel : Set -> Set1
Rel X = X -> X -> Set

data False : Set where
record True : Set where

tt : True
tt = _

! : {A : Set} -> A -> True
! = _

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

subst : {A : Set}(P : A -> Set){x y : A} -> x == y -> P y -> P x
subst P refl p = p

cong : {A B : Set}(f : A -> B){x y : A} -> x == y -> f x == f y
cong f refl = refl

sym : {A : Set}{x y : A} -> x == y -> y == x
sym refl = refl

trans : {A : Set}{x y z : A} -> x == y -> y == z -> x == z
trans refl yz = yz

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

infixr 10 _,_

record Σ (A : Set)(B : A -> Set) : Set where
  field
    fst : A
    snd : B fst

_,,_ : {A : Set}{B : A -> Set}(x : A) -> B x -> Σ A B
x ,, y = record { fst = x; snd = y }

private module Σp {A : Set}{B : A -> Set} = Σ {A}{B}
open Σp public

data _∨_ (A B : Set) : Set where
  inl : A -> A ∨ B
  inr : B -> A ∨ B

data Bool : Set where
  false : Bool
  true  : Bool

IsTrue : Bool -> Set
IsTrue false = False
IsTrue true  = True

IsFalse : Bool -> Set
IsFalse true  = False
IsFalse false = True

data Inspect (b : Bool) : Set where
  itsTrue  : IsTrue b -> Inspect b
  itsFalse : IsFalse b -> Inspect b

inspect : (b : Bool) -> Inspect b 
inspect true  = itsTrue  _
inspect false = itsFalse _

data LeqBool : Rel Bool where
  ref : {b : Bool} -> LeqBool b b
  up  : LeqBool false true

One : Rel True
One _ _ = True

_[×]_ : {A B : Set} -> Rel A -> Rel B -> Rel (A × B)
(R [×] S) (a₁ , b₁) (a₂ , b₂) = R a₁ a₂ × S b₁ b₂