Require Export Functor.

Set Implicit Arguments.
Unset Strict Implicit.


Section idCat.

Variable C : Category.

Definition Id_CAT_ob (a : C) := a.

Definition Id_CAT_map (a b : C) := Id_map (a --> b).

Lemma Id_CAT_comp_law : Fcomp_law (FOb:=Id_CAT_ob) Id_CAT_map.
Proof.
unfold Fcomp_law in |- *; intros; apply Refl.
Qed.

Lemma Id_CAT_id_law : Fid_law (FOb:=Id_CAT_ob) Id_CAT_map.
Proof.
unfold Fid_law, Id_CAT_ob in |- *; intros a; apply Refl.
Qed.

Canonical Structure Id_CAT := Build_Functor Id_CAT_comp_law Id_CAT_id_law.

End idCat.