curryhoward.ctt

module curryhoward where

-- https://queuea9.wordpress.com/2018/10/17/why-i-no-longer-believe-in-computational-classical-type-theory/

data Absurd =

data Either (A : U) (B : U) = Left (a : A)
                            | Right (b : B)

-- law of excluded middle
lem (A : U) : U
  = Either A (A -> Absurd)

data bool = true | false

usefulFunc (A : U) : (l : lem A) -> bool = split
  Left a -> true
  Right aToAbsurd -> false