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 *)