Library CT.Instance.Coq.Category

Require Import CT.Category.

Program Definition CoqType : Category :=
  {| ob := Type;
     mor := fun a b a b;
     comp := fun a b c (f : a b) (g : b c) x g (f x);
     id := fun _ fun x x
  |}.

Program Definition CoqProp : Category :=
  {| ob := Prop;
     mor := fun a b a b;
     comp := fun a b c (f : a b) (g : b c) x g (f x);
     id := fun _ fun x x
  |}.

Program Definition CoqSet : Category :=
  {| ob := Set;
     mor := fun a b a b;
     comp := fun a b c (f : a b) (g : b c) x g (f x);
     id := fun _ fun x x
  |}.