-- some basic data types and functions
module prelude where

import primitives

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

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

subst : (A : U) (P : A -> U) (a x : A) (p : Id A a x) -> P a -> P x
subst A P a x p = transport (P a) (P x) (mapOnPath A U P a 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

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 = transportRef (P a) d

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

N0Dec : discrete N0
N0Dec x y = inl rem
 where rem : Id N0 x y
       rem = efq (Id N0 x y) x

unitDec : discrete Unit
unitDec = split
  tt -> split
          tt -> inl (refl Unit tt)

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 = mapOnPath (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 = mapOnPath (Pi A B) (B a) (\ f -> f a)

J : (A : U) (a : A) (C : (x : A) -> Id A a x -> U) (d: C a (refl A a)) (x : A) (p : Id A a x)
      -> C x p
J A a C d x p = subst (singl A a) T (a, refl A a) (x, p) (contrSingl A a x p) d
 where T : singl A a -> U
       T z = C (z.1) (z.2)

funExt : (A : U) (B : A -> U) (f g : (a : A) -> B a)
         (p : ((x : A) -> (Id (B x) (f x) (g x)))) -> Id ((y : A) -> B y) f g
funExt A B f g p = funHExt A B f g rem
  where rem : (a x : A) -> (p : Id A a x) -> (IdS A B a x p (f a) (g x))
        rem a = J A a (\ x p -> (IdS A B a x p (f a) (g x))) (p a)

tId : (A : U) (a : A) (v : pathTo A a) -> Id (pathTo A a) (sId A a) v
tId A a z = rem (z.1) a (z.2)
   where
    rem : (x y : A) (p : Id A x y) -> Id (pathTo A y) (sId A y) (x, p)
    rem x = J A x (\y p -> Id (pathTo A y) (sId A y) (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 z = equivEq A B f z.1 z.2

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

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 -> mapOnPath 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 -> mapOnPath (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 = (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 = mapOnPath 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))
                       (mapOnPath 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 z = z.1

eqToEucl : (A : U) (R : rel A) -> equivalence A R -> euclidean A R
eqToEucl A R z = z.2

eqToSym : (A : U) (R : rel A) -> equivalence A R -> symmetry A R
eqToSym A R z a b = (z.2) b a b (z.1 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