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 +