From 9c3fbf93fd0b238ec5aedb601c8b149a738f4f7d Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 30 Sep 2023 18:31:47 +0200
Subject: [PATCH] tweak quantities in eta.from-false

---
 examples/eta.quox | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/examples/eta.quox b/examples/eta.quox
index 817bbc3..67d1a8b 100644
--- a/examples/eta.quox
+++ b/examples/eta.quox
@@ -18,8 +18,8 @@ def0 pair : (A : ★) → (B : A → ★) → (P : Σ A B → ★) → (e : Σ A
   λ A B P e p ⇒ p
 
 -- not exactly η, but kinda related
-def0 from-false : (A : ★) → (P : (False → A) → ★) → (f : False → A) →
-                  P (λ x ⇒ void A x) → P f =
+def0 from-false : (A : ★) → (P : (0.False → A) → ★) → (f : 0.False → A) →
+                  P (void A) → P f =
   λ A P f p ⇒ p
 
 }