proposition: Lemma products_unique `{Product c} `{Product c'}: iso_arrows (make_tuple c c' (tuple_proj c')) (make_tuple c' c (tuple_proj c)).
proof: Proof. Proof with intuition. unfold iso_arrows. revert c H1 H2 H3 c' H4 H5 H6. cut (∀ `{Product x} `{Product y}, make_tuple x y (tuple_proj y) ◎ make_tuple y x (tuple_proj x) = cat_id)... pose proof (proj2 (product_factors x x (tuple_proj x))) as Q. rewrite (Q cat_id)... rewrite Q... rewrite associativity. repeat rewrite tuple_round_trip... rewrite right_identity... Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.theory.setoids MathClasses.interfaces.functors MathClasses.theory.jections