hoq-0.1.0.0: examples/basics.hoq

-- Pi types
id : (A : Type) -> A -> A
id A a = a

-- Universes
-- Type and Type0 are synonyms
universes : (f : Type1 -> Type0) -> f Type0 -> f Type0
universes f = id (f Type0)

-- Universes are cumulative
cumulative : Type3 -> Type8
cumulative A = A

-- Lambdas
compose : (A B C : Type) -> (B -> C) -> (A -> B) -> A -> C
compose A B C = \g f a -> g (f a)

-- Data types
data Bool = false | true

data Nat = zero | suc Nat

data List (A : Type) = nil | cons A (List A)

-- Pattern matching
not : Bool -> Bool
not true = false
not false = true

and : Bool -> Bool -> Bool
and true true = true
and _ _ = false

-- Recursive functions
plus : Nat -> Nat -> Nat
plus zero y = y
plus (suc x) y = suc (plus x y)

ack : Nat -> Nat -> Nat
ack zero n = suc n
ack (suc m) zero = ack m (suc zero)
ack (suc m) (suc n) = ack m (ack (suc m) n)

-- Interval type
-- I is a type with constructors left : I and right : I
-- coe and squeeze are primitive operators which satisfy the following rules:
-- 
-- coe : (A : I -> Type) (i : I) -> A i -> (j : I) -> A j
-- coe A i a i = a
-- coe (\_ -> A) i a j = a
-- 
-- squeeze : I -> I -> I
-- squeeze left _ = left
-- squeeze right j = j
-- squeeze _ left = left
-- squeeze i right = i

-- Path types
-- Path A a a' is a type with constructor path : (f : (i : I) -> A i) -> Path A (f left) (f right)
-- a = a' is a synonym for Path (\_ -> A) a a'
-- @ is an eliminator for Path, it has type Path A a a' -> (i : I) -> A i
-- path f @ i = f i

idp : (A : Type) (a : A) -> a = a
idp A a = path (\_ -> a)

transport : (A : Type) (B : A -> Type) (a a' : A) -> a = a' -> B a -> B a'
transport A B _ _ p x = coe (\i -> B (p @ i)) left x right

J : (A : Type) (B : (a a' : A) -> a = a' -> Type) -> ((a : A) -> B a a (idp A a)) -> (a a' : A) (p : a = a') -> B a a' p
J A B d a a' p = coe (\i -> B a (p @ i) (path (\j -> p @ squeeze i j))) left (d a) right

ext : (A : Type) (B : A -> Type) (f g : (a : A) -> B a) -> ((a : A) -> f a = g a) -> f = g
ext A B f g p = path (\i a -> p a @ i)

-- Univalence
not-not : (x : Bool) -> not (not x) = x
not-not true  = idp Bool true
not-not false = idp Bool false

biso : Bool = Bool
biso = path (iso Bool Bool not not not-not not-not)

-- coe satisfies the following rules:
-- coe (iso A B f g p q) left a right = f a
-- coe (iso A B f g p q) right b left = g b
biso-not : coe (\i -> biso @ i) left true right = false
biso-not = idp Bool false

biso-not-not : coe (\i -> biso @ i) right (coe (\i -> biso @ i) left true right) left = true
biso-not-not = idp Bool true

-- Data types with conditions
data Z = positive Nat | negative Nat with
    negative zero = positive zero

-- Now, this works,
succ : Z -> Z
succ (positive x)       = positive (suc x)
succ (negative zero)    = positive (suc zero)
succ (negative (suc x)) = negative x

-- but this don't
succ' : Z -> Z
succ' (positive x)       = positive (suc x)
succ' (negative zero)    = positive zero
succ' (negative (suc x)) = negative x

-- We can define higher inductive types using data types with conditions and the interval object
data Circle = base | loop I with
    loop left  = base
    loop right = base

Circle-elim : (P : Circle -> Type) (b : P base) -> Path (\i -> P (loop i)) b b -> (x : Circle) -> P x
Circle-elim P b t base     = b
Circle-elim P b t (loop i) = t @ i

Circle-elim' : (P : Circle -> Type) (b : P base) -> transport Circle P base base (path loop) b = b -> (x : Circle) -> P x
Circle-elim' P b t base     = b
Circle-elim' P b t (loop i) = 
    coe  (\j -> Path (\k -> P (loop k)) b (t @ j)) left
    (path (\j -> coe (\k -> P (loop k)) left b j)) right @ i