Require Export Functor.

Set Implicit Arguments.
Unset Strict Implicit.


Section constFun.

Variables (A B : Category) (b : B).

Definition Const_ob (a : A) := b.

 Section const_map_def.

 Variable a1 a2 : A.

 Definition Const_mor (f : a1 --> a2) := Id b.

 Lemma Const_mor_map_law : Map_law Const_mor.
 Proof.
 unfold Map_law, Const_mor in |- ×.
 intros f g H; apply Refl.
 Qed.

 Canonical Structure Const_map :
   Map (a1 --> a2) (Const_ob a1 --> Const_ob a1) := Const_mor_map_law.

 End const_map_def.

Lemma Const_comp_law : Fcomp_law Const_map.
Proof.
unfold Fcomp_law, Const_map, Const_mor in |- *; simpl in |- ×.
intros a1 a2 a3 f g; apply Idr.
Qed.

Lemma Const_id_law : Fid_law Const_map.
Proof.
unfold Fid_law, Const_map, Const_mor, Const_ob in |- *; simpl in |- ×.
intros; apply Refl.
Qed.

Canonical Structure Const := Build_Functor Const_comp_law Const_id_law.

End constFun.