From 7f8137b9f6dd57307ca67edba1b4431a04056d3e Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Mon, 8 May 2023 00:39:10 -0500 Subject: [PATCH] add headers --- content/posts/2023-04-21-proving-true-from-false.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/content/posts/2023-04-21-proving-true-from-false.lagda.md b/content/posts/2023-04-21-proving-true-from-false.lagda.md index 062b2ee..c6da9f1 100644 --- a/content/posts/2023-04-21-proving-true-from-false.lagda.md +++ b/content/posts/2023-04-21-proving-true-from-false.lagda.md @@ -71,7 +71,7 @@ compile. It looks like it's not obvious to the interpreter that this statement is actually true. Why is that ---- +## Intuition Well, in constructive logic / constructive type theory, proving something is false is actually a bit different. You see, the definition of the `not` @@ -119,7 +119,7 @@ true≢false2 : true ≢ false true≢false2 p = transport (λ i → bool-map2 (p i)) refl ``` ---- +## Note on proving divergence on equivalent values Let's make sure this isn't broken by trying to apply this to something that's actually true: