Require Export Category.

Set Implicit Arguments.
Unset Strict Implicit.


Lemma Comp_map_congl : Congl_law Comp_map.
Proof.
unfold Congl_law in |- *; simpl in |- *.
unfold Ext in |- *; simpl in |- *.
unfold Comp_fun in |- *; auto.
Qed.

Lemma Comp_map_congr : Congr_law Comp_map.
Proof.
unfold Congr_law in |- *; simpl in |- *.
unfold Ext in |- *; simpl in |- *.
unfold Comp_fun in |- *.
intros a b c f g h e x.
apply Pres1; auto.
Qed.

Definition Comp_SET := Build_Comp Comp_map_congl Comp_map_congr.

Lemma Assoc_SET : Assoc_law Comp_SET.
Proof.
unfold Assoc_law in |- *; simpl in |- *; intros.
unfold Ext in |- *; intro x; simpl in |- *.
apply Refl.
Qed.


Definition Id_SET := Id_map.

Lemma Idl_SET : Idl_law Comp_SET Id_SET.
Proof.
unfold Idl_law in |- *; intros.
unfold Comp in |- *.
unfold Ap2 in |- *; simpl in |- *.
unfold Ext in |- *; simpl in |- *.
intro x; apply Refl.
Qed.

Lemma Idr_SET : Idr_law Comp_SET Id_SET.
Proof.
unfold Idr_law in |- *; intros.
unfold Comp in |- *.
unfold Ap2 in |- *; simpl in |- *.
unfold Ext in |- *; simpl in |- *.
intro x; apply Refl.
Qed.

Canonical Structure SET := Build_Category Assoc_SET Idl_SET Idr_SET.