diff --git a/Data/Profunctor/Yoneda.idr b/Data/Profunctor/Yoneda.idr index badb280..21034b2 100644 --- a/Data/Profunctor/Yoneda.idr +++ b/Data/Profunctor/Yoneda.idr @@ -45,6 +45,11 @@ export yonedaEqv : Profunctor p => p a b <=> Yoneda p a b yonedaEqv = MkEquivalence propure proextract +export +yonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p => + p (q a b) (r a' b') -> p (Yoneda q a b) (Yoneda r a' b') +yonedaIso = dimap proextract propure + export Functor (Yoneda p a) where map = rmap @@ -118,6 +123,11 @@ export coyonedaEqv : Profunctor p => p a b <=> Coyoneda p a b coyonedaEqv = MkEquivalence propure proextract +export +coyonedaIso : (Profunctor q, Profunctor r) => forall p. Profunctor p => + p (q a b) (r a' b') -> p (Coyoneda q a b) (Coyoneda r a' b') +coyonedaIso = dimap proextract propure + export Functor (Coyoneda p a) where map = rmap