Skip to content

Instantly share code, notes, and snippets.

@erutuf

erutuf/HaityuuOishii.agda

Created April 1, 2011 15:20
Show Gist options
  • Save erutuf/898320 to your computer and use it in GitHub Desktop.
Save erutuf/898320 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
HaityuuOishii.agda
module HaityuuOishii where
data False : Set where
data _\/_ (P Q : Set) : Set where
orl : P -> P \/ Q
orr : Q -> P \/ Q
haityu : (P : Set) -> (forall (P : Set) -> ((P -> False) -> False) -> P) -> (P \/ (P -> False))
haityu P nnp = nnp (P \/ (P -> False)) (\ z -> z ((orr (\ x -> z (orl x)))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment