-- some basic data types and functions

module prelude where

import primitive

rel : U -> U
rel A = A -> A -> U

euclidean : (A : U) -> rel A -> U
euclidean A R = (a b c : A) -> R a c -> R b c -> R a b

and : (A B : U) -> U
and A B = Sigma A (\_ -> B)

Pi : (A:U) -> (A -> U) -> U
Pi A B = (x:A) -> B x

fst : (A : U) (B : A -> U) -> Sigma A B -> A
fst A B = split
  pair a b -> a

snd : (A : U) (B : A -> U) (p : Sigma A B) -> B (fst A B p)
snd A B = split
  pair a b -> b

-- some data types

Unit : U
data Unit = tt

N : U
data N = zero | suc (n : N)

Bool : U
data Bool = true | false

andBool : Bool -> Bool -> Bool
andBool = split
  true -> \x -> x
  false -> \x -> false

not : Bool -> Bool
not = split
  true -> false
  false -> true

isEven : N -> Bool
isEven = split
  zero -> true
  suc n -> not (isEven n)

pred : N -> N
pred = split
        zero -> zero
        suc n -> n

subst : (A : U) (P : A -> U) (a x : A) (p : Id A a x) -> P a -> P x
subst A P a x p d = J A a (\ x q -> P x) d x p

substInv : (A : U) (P : A -> U) (a x : A) (p : Id A a x) -> P x -> P a
substInv A P a x p = subst A (\ y -> P y -> P a) a x p (\ h -> h)

substeq : (A : U) (P : A -> U) (a : A) (d : P a) ->
          Id (P a) d (subst A P a a (refl A a) d)
substeq A P a d = Jeq A a (\ x q -> P x) d

cong : (A B : U) (f : A -> B) (a b : A) (p : Id A a b) -> Id B (f a) (f b)
cong A B f a b p = subst A (\x -> Id B (f a) (f x)) a b p (refl B (f a))

N0 : U
data N0 =

efq : (A : U) -> N0 -> A
efq A = split {}

neg : U -> U
neg A = A -> N0

or : U -> U -> U
data or A B = inl (a : A) | inr (b : B)

orElim : (A B C:U) -> (A->C) -> (B -> C) -> or A B -> C
orElim A B C f g = 
 split
  inl a -> f a
  inr b -> g b

dec : U -> U
dec A = or A (neg A)

discrete : U -> U
discrete A = (a b : A) -> dec (Id A a b)

tnotf : neg (Id Bool (true) (false))
tnotf h =
  let
    T : Bool -> U
    T = split
          true  -> N
          false -> N0
  in subst Bool T (true) (false) h (zero)

fnott : neg (Id Bool false true)
fnott h = substInv Bool T false  true h zero
  where
    T : Bool -> U
    T = split
          true  -> N
          false -> N0

boolDec : discrete Bool
boolDec = split
  true -> split
    true -> inl (refl Bool (true))
    false -> inr tnotf
  false -> split
    true -> inr fnott
    false -> inl (refl Bool (false))

notK : (x : Bool) -> Id Bool (not (not x)) x
notK = split
  true  -> refl Bool (true)
  false -> refl Bool (false)

appId : (A B : U) (a : A) (f0 f1 : A -> B) -> Id (A -> B) f0 f1 -> Id B (f0 a) (f1 a)
appId A B a = cong (A->B) B (\ f -> f a) 

appEq : (A :U) (B : A -> U) (a : A) (f0 f1 : Pi A B) -> Id (Pi A B) f0 f1 -> Id (B a) (f0 a) (f1 a)
appEq A B a = cong (Pi A B) (B a) (\ f -> f a) 

sId : (A : U) (a : A) -> pathTo A a
sId A a = pair a (refl A a)

tId : (A : U) (a : A) (v : pathTo A a) -> Id (pathTo A a) (sId A a) v
tId A a = split 
  pair x p -> rem x a p 
  where 
  rem : (x y : A) (p : Id A x y) -> Id (pathTo A y) (sId A y) (pair x p)
  rem x = J A x (\y p -> Id (pathTo A y) (sId A y) (pair x p)) (refl (pathTo A x) (sId A x))

typEquivS : (A B : U) -> (f : A -> B) -> U
typEquivS A B f = (y : B) -> fiber A B f y

typEquivT : (A B : U) -> (f : A -> B) -> (typEquivS A B f) -> U
typEquivT A B f s =  (y : B) -> (v : fiber A B f y) -> Id (fiber A B f y) (s y) v

isEquiv : (A B : U) (f : A -> B) -> U
isEquiv A B f = Sigma (typEquivS A B f) (typEquivT A B f)

isEquivEq : (A B : U) (f : A -> B) -> isEquiv A B f -> Id U A B
isEquivEq A B f = split 
  pair s t -> equivEq A B f s t

-- not needed if we have eta

etaId : (A:U) (B:A -> U) -> (f:Pi A B) -> Id (Pi A B) (\ x -> f x) f
etaId A B f = funExt A B (\ x -> f x) f (\ x -> refl (B x) (f x))

funSplit : (A:U) (B:A->U) (C: (Pi A B) -> U) -> ((f:Pi A B) -> C (\ x -> f x)) -> Pi (Pi A B) C
funSplit A B C eC f = subst (Pi A B) C (\ x -> f x) f (etaId A B f) (eC f)

surjPair : (A:U) (B:A -> U) -> (s:Sigma A B) -> Id (Sigma A B) (pair (fst A B s) (snd A B s)) s
surjPair A B = split
                pair a b -> refl (Sigma A B) (pair a b)

lemProp1 : (A : U) -> (A -> prop A) -> prop A
lemProp1 A h a0 = h a0 a0

propN0 : prop N0
propN0 a b = efq (Id N0 a b) a

-- a product of propositions is a proposition

isPropProd : (A:U) (B:A->U) (pB : (x:A) -> prop (B x)) -> prop (Pi A B)
isPropProd A B pB f0 f1 = funExt A B f0 f1 (\ x -> pB x (f0 x) (f1 x))

propNeg : (A:U) -> prop (neg A)
propNeg A = isPropProd A (\ _ -> N0) (\ _ -> propN0)

lemProp2 : (A : U) -> prop A -> prop (dec A)
lemProp2 A pA  = split
 inl a -> split 
           inl b -> cong A (dec A) (\ x -> inl x) a b (pA a b)
           inr nb -> efq (Id (dec A) (inl a) (inr nb)) (nb a)
 inr na -> split 
           inl b -> efq (Id (dec A) (inr na) (inl b)) (na b)
           inr nb -> cong (neg A) (dec A) (\ x -> inr x) na nb (propNeg A na nb)

singl : (A:U) -> A -> U
singl = pathTo
-- singl = Sigma A (\ x -> Id A x a)

idIsEquiv : (A:U) -> isEquiv A A (id A)
idIsEquiv A = pair (sId A) (tId A)

propUnit : prop Unit
propUnit = split
  tt -> split
     tt -> refl Unit (tt)

sucInj : (n m : N) -> Id N (suc n) (suc m) -> Id N n m
sucInj n m h = cong N N pred (suc n) (suc m) h

decEqCong : (A B : U) (f : A -> B) (g : B -> A) -> dec A -> dec B
decEqCong A B f g = split
  inl a -> inl (f a)
  inr h -> inr (\b -> h (g b))

znots : (n : N) -> neg (Id N (zero) (suc n))
znots n h = subst N T zero (suc n) h zero
  where
    T : N -> U
    T = split
          zero -> N
          suc n -> N0

snotz : (n : N) -> neg (Id N (suc n) zero)
snotz n h = substInv N T (suc n) zero h zero
  where
    T : N -> U
    T = split
          zero -> N
          suc n -> N0

natDec : discrete N
natDec = split
  zero  -> split
    zero -> inl (refl N zero)
    suc m -> inr (znots m)
  suc n -> split
    zero -> inr (snotz n)
    suc m -> decEqCong (Id N n m) (Id N (suc n) (suc m))
                       (cong N N (\ x -> suc x) n m) (sucInj n m) (natDec n m)

propPi : (A : U) (B : A -> U) -> ((x : A) -> prop (B x)) -> prop ((x : A) -> B x)
propPi A B h f0 f1 = funExt A B f0 f1 (\x -> h x (f0 x) (f1 x)) 

propImply : (A B : U) -> (A -> prop B) -> prop (A -> B)
propImply A B h = propPi A (\_ -> B) h

propFam : (A : U) (B : A -> U) -> U
propFam A B = (a : A) -> prop (B a)

reflexive : (A : U) -> rel A -> U
reflexive A R = (a : A) -> R a a

symmetry : (A : U) -> rel A -> U
symmetry A R = (a b : A) -> R a b -> R b a

equivalence : (A : U) -> rel A -> U
equivalence A R = and (reflexive A R) (euclidean A R)

eqToRefl : (A : U) (R : rel A) -> equivalence A R -> reflexive A R
eqToRefl A R = split
  pair r _ -> r

eqToEucl : (A : U) (R : rel A) -> equivalence A R -> euclidean A R
eqToEucl A R = split
  pair _ e -> e

eqToSym : (A : U) (R : rel A) -> equivalence A R -> symmetry A R
eqToSym A R = split
  pair r e -> \a b -> e b a b (r b)

eqToInvEucl : (A : U) (R : rel A) -> equivalence A R ->
              (a b c : A) -> R c a -> R c b -> R a b
eqToInvEucl A R eq a b c p q =
  eqToEucl A R eq a b c (eqToSym A R eq c a p) (eqToSym A R eq c b q)

-- definition by case on a decidable equality
-- needed for Nicolai Kraus example

defCase : (A X:U) -> X -> X -> dec A -> X
defCase A X x0 x1 = 
 split
  inl _ -> x0
  inr _ -> x1

IdDefCasel : (A X:U) (x0 x1 : X) (p : dec A)  -> A -> 
             Id X (defCase A X x0 x1 p) x0
IdDefCasel A X x0 x1 = split
 inl _ -> \ _ -> refl X x0
 inr v -> \ u -> efq (Id X (defCase A X x0 x1 (inr v)) x0) (v u)

IdDefCaser : (A X:U) (x0 x1 : X) (p : dec A)  -> (neg A) -> 
             Id X (defCase A X x0 x1 p) x1
IdDefCaser A X x0 x1 = split
 inl u -> \ v -> efq (Id X (defCase A X x0 x1 (inl u)) x1) (v u)
 inr _ -> \ _ -> refl X x1