The intuitionistic negation example is so mind blowing. I can only wrap my head around it when I think about it in terms of functions and types: not : Type

The intuitionistic negation example is so mind blowing. I can only wrap my head around it when I think about it in terms of functions and types: not : Type -> Type not P = P -> ⊥ modus-ponens : P -> ((f : P -> Q) -> Q) modus-ponens p = λf. f p -- p implies not-not-p not-not : P -> ((f : P -> ⊥) -> ⊥) not-not p = λf. f p -- not-p implies not-not-not-p not-not-not : (P -> ⊥) -> (((P -> ⊥) -> ⊥) -> ⊥) not-not-not np = λf. f np -- not-not-not-p implies not-p not-p : (((P -> ⊥) -> ⊥) -> ⊥) -> (P -> ⊥) not-p nnnp = λp. nnnp (not-not p) Now it all just turns into function application :)