tupleはモノイダル積

http://d.hatena.ne.jp/m-a-o/20110325#p1
の(2)の終わりで、functional extensionalityを仮定しない限り、Coqのtupleは圏論的な意味での直積になってることは言えないと書いた。それでも、モノイダル積にはなってるだろうと思ってたのだけど、実際にCoqで証明してみた。証明自体はCoq初心者の演習問題レベル

当たり前だけど、((a*b)%type*c)%typeと(a*(b*c)%type)%typeは等しくないので、strictでなく、weak monoidal categoryにしかならない。まあ別にcartesian categoryにならなくても、monoidal categoryになればよいかという気がする

(* coq-8.3 *)
(* associator *)
Definition assoc (a b c:Type): ((a*b)%type*c)%type -> (a*(b*c)%type)%type.
  exact (fun x => (fst (fst x),(snd (fst x) , snd x))).
Defined.


Definition par : forall {a b a' b'},(a->a') -> (b->b') -> ((a*b)%type -> (a'*b')%type).
  intros a b a' b' f g x.
  exact (f (fst x) , g (snd x)).
Defined.

Definition comp {a b c} : (a->b) -> (b->c) -> (a->c).
  auto.
Defined.

Notation "f @ g" := (comp f g) (at level 60).

Definition pentagon {a b c d} : 
  (par (assoc a b c) (@id d)) @ (assoc a (b*c)%type d) @ (par (@id a) (assoc b c d)) =
    (assoc (a*b)%type c d) @ (assoc a b (c*d)%type).
  reflexivity.
Defined.


(* unitor *)
Definition runit (a:Type) : (a*unit)%type -> a.
  exact (fun x=>fst x).
Defined.

Definition lunit (a:Type) : (unit*a)%type -> a.
  exact (fun x=>snd x).
Defined.

Definition triangle {a b} : (assoc a unit b) @ (par (@id a) (lunit b)) = (par (runit a) (@id b)).
  reflexivity.
Defined.

(* TODO:分配則のcoherence *)