From af7c222cc3e487cd3ca8b5dd8749b7e258da7c7c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 16 Jun 2023 18:01:33 +0100
Subject: Define semantics and encode types up to pairs.

---
 src/Encoded/Pair.idr | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 src/Encoded/Pair.idr

(limited to 'src/Encoded/Pair.idr')

diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
new file mode 100644
index 0000000..b2a95ab
--- /dev/null
+++ b/src/Encoded/Pair.idr
@@ -0,0 +1,25 @@
+module Encoded.Pair
+
+import Encoded.Bool
+import Encoded.Union
+import Term.Syntax
+
+export
+(*) : Ty -> Ty -> Ty
+ty1 * ty2 = B ~> (ty1 <+> ty2)
+
+export
+pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
+pair = Abs $ Abs $ Abs $
+  let t = Var (There $ There Here) in
+  let u = Var (There Here) in
+  let b = Var Here in
+  App if' [<b, App inL [<t], App inR [<u]]
+
+export
+fst : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty1) ctx
+fst = Abs $ App (prL . Var Here) [<True]
+
+export
+snd : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty2) ctx
+snd = Abs $ App (prR . Var Here) [<False]
-- 
cgit v1.2.3