Require Export Category.

Set Implicit Arguments.
Unset Strict Implicit.

Section fscat.

Variables (C : Category) (I : Type) (a : I → C).

Definition FSC_mor_setoid (i j : I) := a i --> a j.


Definition Comp_FSC (i j l : I) :
  Map2 (FSC_mor_setoid i j) (FSC_mor_setoid j l) (FSC_mor_setoid i l) :=
  Op_comp (a i) (a j) (a l).

Lemma Assoc_FSC : Assoc_law Comp_FSC.
Proof.
unfold Assoc_law in |- *; intros i1 i2 i3 i4 f g h.
exact (Ass f g h).
Qed.


Definition Id_FSC (i : I) := Id (a i).

Lemma Idl_FSC : Idl_law Comp_FSC Id_FSC.
Proof.
unfold Idl_law in |- *; intros i j f.
exact (Idl f).
Qed.

Lemma Idr_FSC : Idr_law Comp_FSC Id_FSC.
Proof.
unfold Idr_law in |- *; intros i j f.
exact (Idr f).
Qed.

Canonical Structure FullSubCat := Build_Category Assoc_FSC Idl_FSC Idr_FSC.

End fscat.