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

-- Implicit arguments
id' : {A : Type} -> A -> A
id' _ a = a

test : (A : Type) -> (A -> A) -> (A -> A)
test _ f = id' f

-- 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
and : Bool -> Bool -> Bool
and true true = true
and _ _ = false

-- Case construction
not : Bool -> Bool
not b = case b of
    true -> false
    false -> true

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

-- Infix operators
infixl 60 `plus`
infixl 70 *
(*) : Nat -> Nat -> Nat
(*) zero _ = zero
(*) (suc x) y = y `plus` x * y

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

-- There are three special subuniverses of Type: Contr, Prop, and Set_i
-- For each A : Contr, we have contr : A
-- A path in Set belongs to Prop, and a path in Prop belongs to Contr, that is
-- Path : (A : I -> Set) -> A left -> A right -> Prop
-- Path : (A : I -> Prop) -> A left -> A right -> Contr
-- Data types which use only types in Set (note that I does not belong to Set) also belong to Set
Nat-isSet : (x y : Nat) (p q : x = y) -> p = q
Nat-isSet _ _ _ _ = contr

-- 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 (coe (\k -> P (loop k)) left b)) right @ i

-- Records
record Sigma (A : Type) (B : A -> Type) where
    constructor (,) -- Constructor can be omitted
    proj1 : A
    proj2 : B proj1

-- We can define path types using records with conditions
-- The only difference between this definition and the built-in one is
-- that this one does not work well with Set, Prop, and Contr.
record Path' (A : I -> Type) (a : A left) (a' : A right) where
    constructor path'
    at : (i : I) -> A i
  with
    at left  = a
    at right = a'