# categories.product

Require Import
Relation_Definitions
abstract_algebra ChoiceFacts interfaces.functors
theory.categories categories.categories.

Section object.
Context {I: Type} (O: I Type)
`{ i, Arrows (O i)}
`{ i (x y: O i), Equiv (x y)}
`{ i, CatId (O i)} `{ i, CatComp (O i)}
`{ i, Category (O i)}.

Definition Object := i, O i.
Global Instance pa: Arrows Object := λ x y, i, x i y i.   Global Instance: CatId Object := λ _ _, cat_id.
Global Instance: CatComp Object := λ _ _ _ d e i, d i e i.
Definition e (x y: Object): Equiv (x y) := λ f g, i, f i = g i.
End object.

Hint Extern 0 (Equiv (_ _)) => eapply @e : typeclass_instances.

Section contents.
Context {I: Type} (O: I Type)
`{ i, Arrows (O i)}
`{ i (x y: O i), Equiv (x y)}
`{ i, CatId (O i)} `{ i, CatComp (O i)}
`{ i, Category (O i)}.

Global Instance: x y: Object O, Setoid (x y) := {}.

Global Instance: Category (Object O).

Let product_object := categories.object (Object O).

Notation ith_obj i := (categories.object (O i)).

Program Definition project i: categories.object (Object O) ith_obj i :=
categories.arrow (λ d, d i) (λ _ _ a, a i) _.

Section factors.

Variables (C: categories.Object) (X: i, C ith_obj i).

Let ith_functor i := categories.Functor_inst _ _ (X i).

Program Definition factor: C product_object
:= categories.arrow (λ (c: C) i, X i c) (λ (x y: C) (c: x y) i, fmap (X i) c) _.
End factors.

Global Instance mono (X Y: Object O): (a: X Y), ( i, @Mono _ _ (H0 _) (H2 i) _ _ (a i)) Mono a.

End contents.