module BoolEqBool where

import equivSet
import hedberg

notInj : (x y : Bool) -> Id Bool (not x) (not y) -> Id Bool x y
notInj x y p = compUp Bool (not (not x)) x (not (not y)) y (notK x) (notK y) rem
  where
  rem : Id Bool (not (not x)) (not (not y))
  rem = mapOnPath Bool Bool not (not x) (not y) p

notFiber : Bool -> U
notFiber b = fiber Bool Bool not b

eqNotFiber : (b : Bool) -> (v v' : notFiber b) ->
             Id Bool v.1 v'.1 -> Id (notFiber b) v v'
eqNotFiber b = eqPropFam Bool (\x -> Id Bool (not x) b)
                              (\x -> boolIsSet (not x) b)

sNot : (b : Bool) -> notFiber b
sNot b = (not b, notK b)

tNot : (b : Bool) (v : notFiber b) -> Id (notFiber b) (sNot b) v
tNot b v = eqNotFiber b (sNot b) v rem
  where
  rem1 : Id Bool (not (not b)) (not v.1)
  rem1 = comp Bool (not (not b)) b (not v.1) (notK b)
         (inv Bool (not v.1) b v.2)

  rem : Id Bool (not b) v.1
  rem = notInj (not b) v.1 rem1

eqBoolBool : Id U Bool Bool
eqBoolBool = equivEq Bool Bool not sNot tNot

transportInv : (A B : U) -> Id U A B -> B -> A
transportInv = substInv U (\x -> x)

notEqBool : Bool -> Bool
notEqBool = transport Bool Bool eqBoolBool

testBool : Bool
testBool = notEqBool true

compEqBool : Id U Bool Bool
compEqBool = comp U Bool Bool Bool eqBoolBool eqBoolBool

transport' : (A B : U) -> Id U A B -> A -> B
transport' = subst U (\x -> x)

funCompEqBool : Bool -> Bool
funCompEqBool = transport' Bool Bool compEqBool

newTestBool : Bool
newTestBool = funCompEqBool (true)

newCompEqBool : Id U Bool Bool
newCompEqBool = comp U Bool Bool Bool eqBoolBool (refl U Bool)

test2Bool : Bool
test2Bool = transport' Bool Bool newCompEqBool (true)

monoid : U -> U
monoid A = and A (A -> A -> A)

zm : (A : U) (m : monoid A) -> A
zm A m = m.1

opm : (A : U) (m : monoid A) -> (A -> A -> A)
opm A m = m.2

transm : (A B : U) -> Id U A B -> monoid A -> monoid B
transm = subst U monoid

transun : (A B : U) -> Id U A B -> (A -> A) -> (B -> B)
transun = subst U (\X -> (X -> X))

transid : Bool -> Bool
transid = transun Bool Bool eqBoolBool (\x -> x)

testT : Bool
testT = transid true

testT' : Bool
testT' = transun Bool Bool (refl U Bool) (\x -> x) true

testF : Bool
testF = transid false

monoidAndBool : monoid Bool
monoidAndBool = (true, andBool)

mBool2 : monoid Bool
mBool2 = transm Bool Bool eqBoolBool monoidAndBool

opBool2 : Bool -> Bool -> Bool
opBool2 = opm Bool mBool2

testTF : Bool
testTF = opBool2 true false

testFT : Bool
testFT = opBool2 false true

testFF : Bool
testFF = opBool2 false false

testTT : Bool
testTT = opBool2 true true

-- Bool tests:

equivBool : Id U Bool Bool
equivBool = equivSet Bool Bool not not notK notInj boolIsSet

mBool3 : monoid Bool
mBool3 = transm Bool Bool equivBool monoidAndBool

opBool3 : Bool -> Bool -> Bool
opBool3 = opm Bool mBool3

testTF3 : Bool
testTF3 = opBool3 true false

testFT3 : Bool
testFT3 = opBool3 false true

testFF3 : Bool
testFF3 = opBool3 false false

testTT3 : Bool
testTT3 = opBool3 true true

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

testTT4 : Id Bool (orBool false true) (opBool3 false true)
testTT4 = refl Bool true