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