module nIso where

import univalence

-- an example with N and 1 + N isomorphic

NToOr : N -> or N Unit
NToOr = split
           zero -> inr tt
           suc n -> inl n

OrToN : or N Unit -> N
OrToN = split
            inl n -> suc n
            inr _ -> zero

secNO : (x:N) -> Id N (OrToN (NToOr x)) x
secNO = split
         zero -> refl N zero
         suc n -> refl N (suc n)

retNO : (z:or N Unit) -> Id (or N Unit) (NToOr (OrToN z)) z
retNO = split
         inl n -> refl (or N Unit) (inl n)
         inr y -> lem y
              where lem : (y:Unit) -> Id (or N Unit) (inr tt) (inr y)
                    lem = split
                            tt -> refl (or N Unit) (inr tt)

isoNO : Id U N (or N Unit)
isoNO = isoId N (or N Unit) NToOr OrToN retNO secNO

-- trying to build an example which involves Kan filling for product

vect : U -> N -> U
vect A = split
          zero -> A 
          suc n -> and A (vect A n)

pBool : N -> U
pBool = vect Bool

notSN : (x:N) -> pBool x -> pBool x
notSN = split
         zero -> not
         suc n -> split
                    pair b u -> pair (not b) (notSN n u)

sBool : (x:N) -> pBool x
sBool = split
        zero -> true
        suc n -> pair false (sBool n)

stBool : (x:N) -> pBool x -> Bool
stBool = split
           zero -> \ z -> z
           suc n -> split
                      pair b u -> andBool b (stBool n u)

hasSec : U -> U
hasSec X = Sigma (X->U) (\ P -> (x:X) -> and (P x) (P x -> Bool))

hSN : hasSec N
hSN = pair pBool (\ n -> pair (sBool n) (stBool n))

hSN' : hasSec (or N Unit)
hSN' = subst U hasSec N (or N Unit) isoNO hSN

pB' : (or N Unit) -> U
pB' = fst ((or N Unit) -> U)  (\ P -> (x:or N Unit) -> and (P x) (P x -> Bool)) hSN'

sB' : (z: or N Unit) -> and (pB' z) (pB' z -> Bool)
sB' = snd ((or N Unit) -> U)  (\ P -> (x:or N Unit) -> and (P x) (P x -> Bool)) hSN'

appBool : (A : U) -> and A (A -> Bool) -> Bool
appBool A = split
             pair a f -> f a

pred' : or N Unit -> or N Unit
pred' = subst U (\ X -> X -> X) N (or N Unit) isoNO pred

testPred : or N Unit
testPred = pred' (inr tt)

saB' : or N Unit -> Bool
saB' z = appBool (pB' z) (sB' z)

testSN : Bool
testSN = saB' (inr tt)

testSN1 : Bool
testSN1 = saB' (inl zero)

testSN2 : Bool
testSN2 = saB' (inl (suc zero))

testSN3 : Bool
testSN3 = saB' (inl (suc (suc zero)))

add : N -> N -> N
add x = split 
         zero -> x
         suc y -> suc (add x y)

-- add' : (or N Unit) -> (or N Unit) -> or N Unit
-- add' = subst U (\ X -> X -> X -> X) N (or N Unit) isoNO add


-- a property that we can transport

propAdd : (x:N) -> Id N (add zero x) x
propAdd = split
           zero -> refl N zero
           suc n -> cong N N (\ x -> suc x) (add zero n) n (propAdd n)
-- propAdd' : (z:or N Unit) 




-- a property of N

aZero : U -> U
aZero X = Sigma X (\ z -> Sigma (X -> X -> X) (\ f -> (x:X) -> Id X (f z x) x))

aZN : aZero N
aZN = pair zero (pair add propAdd)

aZN' : aZero (or N Unit)
aZN' = subst U aZero N (or N Unit) isoNO aZN

zero' : or N Unit
zero' = fst (or N Unit) (\ z -> Sigma ((or N Unit) -> (or N Unit) -> (or N Unit)) 
                                 (\ f -> (x:(or N Unit)) -> Id (or N Unit) (f z x) x)) aZN'

sndaZN' : Sigma ((or N Unit) -> (or N Unit) -> (or N Unit)) 
                                 (\ f -> (x:(or N Unit)) -> Id (or N Unit) (f zero' x) x)
sndaZN' = snd (or N Unit) (\ z -> Sigma ((or N Unit) -> (or N Unit) -> (or N Unit)) 
                                 (\ f -> (x:(or N Unit)) -> Id (or N Unit) (f z x) x)) aZN'

add' : (or N Unit) -> (or N Unit) -> or N Unit
add' = fst ((or N Unit) -> (or N Unit) -> (or N Unit)) 
                                 (\ f -> (x:(or N Unit)) -> Id (or N Unit) (f zero' x) x) sndaZN'

propAdd' : (x:or N Unit) -> Id (or N Unit) (add' zero' x) x
propAdd' = snd ((or N Unit) -> (or N Unit) -> (or N Unit)) 
                                 (\ f -> (x:(or N Unit)) -> Id (or N Unit) (f zero' x) x) sndaZN'


testNO : or N Unit
testNO = add' (inl zero) (inl (suc zero))

testNO1 : Id (or N Unit) (add' zero' zero') zero'
testNO1 = propAdd' zero'