idris2-profunctors/Data/Profunctor/Functor.idr

56 lines
1.9 KiB
Idris
Raw Permalink Normal View History

2023-03-07 22:15:08 -05:00
||| This module defines endofunctors in the category of profunctors `[Idrᵒᵖ * Idr, Idr]`,
||| along with adjunctions of those functors.
||| Examples of these functors include `Yoneda`, `Pastro`, `Closure`, etc.
2023-03-04 23:57:12 -05:00
module Data.Profunctor.Functor
import Data.Profunctor.Types
%default total
2023-03-07 22:15:08 -05:00
||| An endofunctor in the category of profunctors.
|||
||| Laws:
||| * `promap id = id`
||| * `promap g . promap f = promap (g . f)`
2023-03-04 23:57:12 -05:00
public export
interface ProfunctorFunctor (0 t : (Type -> Type -> Type) -> k -> k' -> Type) where
2023-03-07 22:15:08 -05:00
||| Lift a transformation between profunctors into the functor `t`.
2023-03-04 23:57:12 -05:00
promap : Profunctor p => p :-> q -> t p :-> t q
2023-03-07 22:15:08 -05:00
||| A monad in the category of profunctors.
|||
||| Laws:
||| * `projoin . proreturn ≡ id`
||| * `projoin . promap proreturn ≡ id`
||| * `projoin . projoin ≡ projoin . promap projoin`
2023-03-04 23:57:12 -05:00
public export
2023-03-05 00:00:50 -05:00
interface ProfunctorFunctor t =>
ProfunctorMonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
2023-03-04 23:57:12 -05:00
propure : Profunctor p => p :-> t p
projoin : Profunctor p => t (t p) :-> t p
2023-03-07 22:15:08 -05:00
||| A comonad in the category of profunctors.
|||
||| Laws:
||| * `proextract . produplicate ≡ id`
||| * `promap proextract . produplicate ≡ id`
||| * `produplicate . produplicate ≡ promap produplicate . produplicate`
2023-03-04 23:57:12 -05:00
public export
2023-03-05 00:00:50 -05:00
interface ProfunctorFunctor t =>
ProfunctorComonad (0 t : (Type -> Type -> Type) -> Type -> Type -> Type) where
2023-03-04 23:57:12 -05:00
proextract : Profunctor p => t p :-> p
produplicate : Profunctor p => t p :-> t (t p)
2023-03-05 00:00:50 -05:00
2023-03-07 22:15:08 -05:00
||| An adjunction between endofunctors in the category of profunctors.
|||
||| Laws:
||| * `counit . promap unit ≡ id`
||| * `promap counit . unit ≡ id`
2023-03-05 00:00:50 -05:00
public export
2023-03-07 22:15:08 -05:00
interface (ProfunctorFunctor l, ProfunctorFunctor r) =>
ProfunctorAdjunction (0 l, r : (Type -> Type -> Type) -> Type -> Type -> Type) | l, r where
prounit : Profunctor p => p :-> r (l p)
procounit : Profunctor p => l (r p) :-> p