From f0f44fe7815435836bc625e837e891188ae8d801 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 22 Jan 2024 12:11:20 +0000
Subject: Fix some bug?

I don't really know. I haven't read this in a long time.
---
 src/Encoded/Pair.idr | 5 +++++
 1 file changed, 5 insertions(+)

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

diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
index 5873e40..4b66cfe 100644
--- a/src/Encoded/Pair.idr
+++ b/src/Encoded/Pair.idr
@@ -38,6 +38,11 @@ bimap = Abs $ Abs $ Abs $ Abs $
     , App (inR . g . prR . x) [<False]
     ]
 
+export
+mapFst : {ty1, ty1', ty2 : Ty} -> Term ((ty1 ~> ty1') ~> ty1 * ty2 ~> ty1' * ty2) ctx
+mapFst = AbsAll [<_,_] (\[<f, x] =>
+  App pair [<App (f . fst) [<x], App snd [<x]])
+
 export
 mapSnd : {ty1, ty2, ty2' : Ty} -> Term ((ty2 ~> ty2') ~> ty1 * ty2 ~> ty1 * ty2') ctx
 mapSnd = Abs $ Abs $
-- 
cgit v1.2.3