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.