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
  |}.