Add an encoding of Leibniz equality as an example

1ml-prime · Jul 27, 2020 · 34c712c · 34c712c
1 parent 00d4c3c
commit 34c712c
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 0 deletions.
diff --git a/examples/leibniz.1ml b/examples/leibniz.1ml
@@ -0,0 +1,10 @@
+local import "prelude"
+
+type t a b = wrap (type p _) -> p a -> p b
+
+id (type p _) = Fun.id
+((bc: t _ _) << (ab: t _ _)) (type p _) x = bc p (ab p x)
+invert (eq: t _ _) (type p _) = eq (type fun b => wrap p b -> p _) Fun.id
+
+to (eq: t _ _) = eq (type fun x => x)
+from eq = to (invert eq)
diff --git a/examples/leibniz.1mls b/examples/leibniz.1mls
@@ -0,0 +1,10 @@
+type t a b
+
+type a ~ b = t a b
+
+id 'a: a ~ a                           ;; Reflexivity
+(<<) 'a 'b 'c: b ~ c -> a ~ b -> a ~ c ;; Transitivity
+invert 'a 'b: a ~ b -> b ~ a           ;; Symmetry
+
+to   'a 'b: a ~ b -> a -> b
+from 'a 'b: a ~ b -> b -> a