From af4539e34494e33792f1d22bdef1c50cfe6aa06c Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Mon, 6 Mar 2023 12:32:34 -0500
Subject: [PATCH] Define Closure and Environment

---
 Data/Profunctor/Closed.idr | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/Data/Profunctor/Closed.idr b/Data/Profunctor/Closed.idr
index b656da0..3467f2d 100644
--- a/Data/Profunctor/Closed.idr
+++ b/Data/Profunctor/Closed.idr
@@ -10,3 +10,19 @@ import Data.Profunctor.Strong
 public export
 interface Profunctor p => Closed p where
   closed : p a b -> p (x -> a) (x -> b)
+
+
+-- Closure
+
+public export
+record Closure p a b where
+  constructor MkClosure
+  getClosure : forall x. p (x -> a) (x -> b)
+
+
+-- Environment
+
+public export
+data Environment : (p : Type -> Type -> Type) -> Type -> Type -> Type where
+  MkEnv : ((z -> y) -> b) -> p x y -> (a -> z -> x) -> Environment p a b
+