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

isoNO2 : Id U N (or N Unit)
isoNO2 = comp U N N (or N Unit) (comp U N (or N Unit) N isoNO (inv U N (or N Unit) isoNO)) isoNO

isoNO4 : Id U N (or N Unit)
isoNO4 = comp U N N (or N Unit) (comp U N (or N Unit) N isoNO2 (inv U N (or N Unit) isoNO2)) isoNO2

-- 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 -> \ z -> (not z.1,notSN n z.2)

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

stBool : (x:N) -> pBool x -> Bool
stBool = split
           zero -> \ z -> z
           suc n -> \ z -> andBool z.1 (stBool n z.2)

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

hSN : hasSec N
hSN = (pBool,\ n -> (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' = hSN'.1

sB' : (z: or N Unit) -> and (pB' z) (pB' z -> Bool)
sB' = hSN'.2

appBool : (A : U) -> and A (A -> Bool) -> Bool
appBool A z = z.2 z.1

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 -> mapOnPath N N (\ x -> suc x) (add zero n) n (propAdd n)




-- 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 =  (zero,(add,propAdd))

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

zero' : or N Unit
zero' = aZN'.1

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' = aZN'.2

add' : (or N Unit) -> (or N Unit) -> or N Unit
add' = sndaZN'.1

propAdd' : (x:or N Unit) -> Id (or N Unit) (add' zero' x) x
propAdd' = sndaZN'.2

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

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

testNO2 : or N Unit
testNO2 = zero'

testNO3 : or N Unit
testNO3 = add' zero' zero'

step : U -> U
step X = or X Unit

lemIt : (A:U) (f:A->A) (a:A) -> Id A a (f a) -> Id A a (f (f a))
lemIt A f a p = subst A (\ z -> Id A a (f z)) a (f a) p p

isoNOIt : Id U N (step (step N))
isoNOIt = lemIt U step N isoNO

isoNOIt2 : Id U N (step (step (step (step N))))
isoNOIt2 = lemIt U (\ x -> step (step x)) N isoNOIt

aZNIt : aZero (step (step N))
aZNIt = subst U aZero N (step (step N)) isoNOIt aZN

zeroIt : step (step N)
zeroIt = aZNIt.1

sndaZNIt : Sigma ((step (step N)) -> (step (step N)) -> (step (step N)))
           (\ f -> (x:(step (step N))) -> Id (step (step N)) (f zeroIt x) x)
sndaZNIt = aZNIt.2

addIt : (step (step N)) -> (step (step N)) -> step (step N)
addIt = sndaZNIt.1

propAddIt : (x:step (step N)) -> Id (step (step N)) (addIt zeroIt x) x
propAddIt = sndaZNIt.2

testIt : step (step N)
testIt = addIt (inl (inl zero)) (inl (inl (suc zero)))

testIt1 : Id (step (step N)) (addIt zeroIt zeroIt) zeroIt
testIt1 = propAddIt zeroIt

testIt2 : step (step N)
testIt2 = zeroIt

testIt3 : step (step N)
testIt3 = addIt zeroIt zeroIt

step4 : U -> U
step4 x = step (step (step (step x)))

aZNIt2 : aZero (step4 N)
aZNIt2 = subst U aZero N (step4 N) isoNOIt2 aZN

zeroIt2 : step4 N
zeroIt2 = aZNIt2.1

sndaZNIt2 : Sigma ((step4 N) -> (step4 N) -> (step4 N))
                                 (\ f -> (x:(step4 N)) -> Id (step4 N) (f zeroIt2 x) x)
sndaZNIt2 = aZNIt2.2

addIt2 : (step4 N) -> (step4 N) -> step4 N
addIt2 = sndaZNIt2.1

propAddIt2 : (x:step4 N) -> Id (step4 N) (addIt2 zeroIt2 x) x
propAddIt2 = sndaZNIt2.2

inl4 : N -> step4 N
inl4 x = inl (inl (inl (inl x)))

testIt2 : step4 N
testIt2 = addIt2 (inl4 zero) (inl4 zero)

testIt21 : Id (step4 N) (addIt2 zeroIt2 zeroIt2) zeroIt2
testIt21 = propAddIt2 zeroIt2

testIt22 : step4 N
testIt22 = zeroIt2

testIt23 : step4 N
testIt23 = addIt2 zeroIt2 zeroIt2