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 = cong Bool Bool not (not x) (not y) p

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

fstNotFiber : (b : Bool) -> notFiber b -> Bool
fstNotFiber b = fst Bool (\x -> Id Bool (not x) b)

eqNotFiber : (b : Bool) -> (v v' : notFiber b) ->
  Id Bool (fstNotFiber b v) (fstNotFiber b v') -> Id (notFiber b) v v'
eqNotFiber b = eqPropFam Bool (\x -> Id Bool (not x) b) rem
  where
  rem : propFam Bool (\x -> Id Bool (not x) b)
  rem = \x -> boolIsSet (not x) b

sNot : (b : Bool) -> notFiber b
sNot b = pair (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
  b' : Bool
  b' = fstNotFiber b v

  rem1 : Id Bool (not (not b)) (not b')
  rem1 = comp Bool (not (not b)) b (not b') (notK b)
         (inv Bool (not b') b (snd Bool (\x -> Id Bool (not x) b) v))

  rem : Id Bool (not b) b'
  rem = notInj (not b) b' 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 = fst A (\x -> A -> A -> A) m

opm : (A : U) (m : monoid A) -> (A -> A -> A)
opm A m = snd A (\x -> A -> A -> A) m

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)

True : Bool
True = true

False : Bool
False = false

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 = pair (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