Cat.pts

language fomega;

/* the category of fomega types and functions. */
module Cat;

/* OBJECTS AND ARROWS */

/* objects are types. */
Obj = *;

/* arrows are functions. */
Hom (A B : Obj) : * =
  A -> B;

/* identity arrows. */
id (A : Obj) : Hom A A =
  lambda a . a;

/* arrow composition. */
comp (A B C : Obj) : Hom B C -> Hom A B -> Hom A C =
  lambda f g a . f (g a);

/* FUNCTORS */

/* action of functors on objects */
Functor = Obj -> Obj;

/* action of functors on arrows */
Map (F : Functor) : * =
  Pi A B : Obj . Hom A B -> Hom (F A) (F B);

/* action of bifunctors on objects */
Bifunctor = Obj -> Obj -> Obj;

/* action of bifunctors on arrows */
Bimap (F : Bifunctor) : * =
  Pi A B C D : Obj . Hom A C -> Hom B D -> Hom (F A B) (F C D);

/* MONADS */

/* type of monadic return */
Return (F : Functor) : * =
  Pi A : Obj . Hom A (F A);

/* type of monadic bind */
Bind (F : Functor) : * =
  Pi A B : Obj . Hom A (F B) -> Hom (F A) (F B);

/* type of monadic join */
Join (F : Functor) : * =
  Pi A : Obj . Hom (F (F A)) (F A);

/* bind in terms of map and join */
bind (F : Functor) (map : Map F) (join: Join F) : Bind F =
  lambda A B f .
    comp (F A) (F (F B)) (F B)
      (join B)
      (map A (F B) f);

/* map in terms of bind and return */
map (F : Functor) (return : Return F) (bind : Bind F) : Map F =
  lambda A B f .
    bind A B (comp A B (F B) (return B) f);

/* join in terms of bind and return */
join (F : Functor) (return : Return F) (bind : Bind F) : Join F =
  lambda A .
    bind (F A) A (id (F A));

/* MODULE EXPORTS */

export Obj;
export Hom;
export id;
export comp;
export Functor;
export Map;
export Bifunctor;
export Bimap;
export Return;
export Bind;
export Join;
export bind;
export map;
export join;