hoq-0.1.0.0: examples/lem.hoq

data E
data S = s
data B = true | false

E-elim : (A : Type) -> E -> A
E-elim A ()

T : B -> Type
T true  = S
T false = E

not : B -> B
not true  = false
not false = true

not-not : (x : B) -> not (not x) = x
not-not true  = path (\_ -> true)
not-not false = path (\_ -> false)

biso : I -> Type
biso i = iso B B not not not-not not-not i

not-eq : (b : B) -> not b = b -> E
not-eq true  p = coe (\i -> T (p @ i)) right s left
not-eq false p = coe (\i -> T (p @ i)) left  s right

transport : (A : Type) (B : A -> Type) (a a' : A) -> a = a' -> B a -> B a'
transport A B _ _ p x = coe (\i -> B (p @ i)) left x right

comp : (A : Type) (a a' a'' : A) -> a = a' -> a' = a'' -> a = a''
comp A a a' a'' p q = transport A (\x -> a = x) a' a'' q p

not-lem : ((A : Type) -> ((A -> E) -> E) -> A) -> E
not-lem f = not-eq (f B (\g -> g true))
    (comp B (not (f B (\g -> g true))) (f B (\g -> g false)) (f B (\g -> g true))
        (path (\i -> coe biso i (f (biso i) (\g -> g (coe biso left true i))) right))
        (path (\i -> f B (\g -> g (E-elim (false = true) (g true) @ i)))))