Idris2Doc : Data.Profunctor.Representable

Data.Profunctor.Representable

(source)

Definitions

interfaceRepresentable : (Type->Type->Type) -> (Type->Type) ->Type
  A profunctor `p` is representable if it is isomorphic to `Star f` for some `f`.

Parameters: p, f
Constraints: Sieve p f, Strong p
Methods:
tabulate : (a->fb) ->pab

Implementations:
RepresentableMorphismIdentity
Functorf=>Representable (Kleislimorphismf) f
Functorf=>Representable (Starf) f
Representable (Forgetr) (Constr)
tabulate : Representablepf=> (a->fb) ->pab
Totality: total
Visibility: public export
interfaceCorepresentable : (Type->Type->Type) -> (Type->Type) ->Type
  A profunctor `p` is corepresentable if it is isomorphic to `Costar f` for some `f`.

Parameters: p, f
Constraints: Cosieve p f
Methods:
cotabulate : (fa->b) ->pab

Implementations:
CorepresentableMorphismIdentity
Functorf=>Corepresentable (Costarf) f
Corepresentable (Coforgetr) (Constr)
cotabulate : Corepresentablepf=> (fa->b) ->pab
Totality: total
Visibility: public export
tabulated : (Representableqf, Representablerg) =>Profunctorp=>p (qab) (ra'b') ->p (a->fb) (a'->gb')
Totality: total
Visibility: export
cotabulated : (Corepresentableqf, Corepresentablerg) =>Profunctorp=>p (qab) (ra'b') ->p (fa->b) (ga'->b')
Totality: total
Visibility: export