Library CT.Instance.Functor.ProductFunctor

Require Import CT.Category.
Require Import CT.Functor.
Require Export CT.Instance.Functor.Bifunctor.
Require Import CT.Instance.Functor.Endofunctor.

A product functor \(F\) on a category \(C\) is a Bifunctor: \(F : C \times C \to C\).

Program Definition ProductFunctor (C : Category) := Bifunctor C C C.

This is just an alias for ProductFunctor. It is often used as a tensor product.

Definition Tensor := ProductFunctor.

The endofunctor \(- \otimes y\) for a given tensor functor \(t\) and given \(y \in Ob(C)\).

Program Definition _tensor {C : Category} (t : Tensor C) (y : @ob C)
  : Endofunctor C :=
  {| F_ob := fun a ⇒ F_ob t (a , y );
     F_mor := fun _ _ f ⇒ bimap f id
  |}.
Proof.
Next Obligation.
  unfold bimap.
  destruct t.
  simpl.
  rewrite F_id_law.
  trivial.
Qed.
Next Obligation.
  destruct t.
  simpl.
  rewrite <- F_comp_law.
  simpl.
  rewrite id_left.
  trivial.
Qed.

The endofunctor \(y \otimes -\) for a given tensor functor \(t\) and given \(y \in Ob(C)\).

Program Definition tensor_ {C : Category} (t : Tensor C) (y : @ob C)
  : Endofunctor C :=
  {| F_ob := fun a ⇒ F_ob t (y , a );
     F_mor := fun _ _ f ⇒ bimap id f
  |}.
Proof.
Next Obligation. apply _tensor_obligation_1. Qed.
Next Obligation.
  destruct t.
  simpl.
  rewrite <- F_comp_law.
  simpl.
  rewrite id_left.
  trivial.
Qed.