Or you can think of this in logical terms as the equivalenceα = (α → ο) → ο

I can prove this easily with classical logic, but I had trouble finding resources presenting the axioms and standard equivalences of intuitionistic logic, and I don't feel like trying to come up with a correct, intuitionistic derivation.α = (α ⇒ ο) ⇒ ο

The derivation of disjoint unions as pure arrow types is simple, at least using the normal rules of classical logic:

Notice how the currying makes much more sense than it did last time, now that the second occurrence of the result type is there. Implication and conjunction are obviously not equivalent (duh)! But you can curry a conjunction that occurs on the left-hand side of an implication.α ∨ β

= ((α ∨ β) ⇒ ο) ⇒ ο

= ((α ⇒ ο) ∧ (β ⇒ ο)) ⇒ ο

= (α ⇒ ο) ⇒ (β ⇒ ο) ⇒ ο

Again, I'm not sure how hard this is to prove intuitionistically. But assuming that goes through okay, we get the type equivalence:

α + β = (α → ο) → (β → ο) → ο

## No comments:

Post a Comment