proposition: Lemma Prf_unique_together1 : Unique_together_law Proj1_prod1 Proj2_prod1 Op_together1.
proof: Proof. unfold Unique_together_law in |- *; intros c h. unfold Together_prod, Ap2 in |- *; simpl in |- *; unfold Together1 in |- *. apply Sym. apply (Prf_isCoUA_law2 ua' (f:=Build_Pmor (u:=Build_POb c c) (t:=Build_POb a b) (h o Proj1_prod1) (h o Proj2_prod1)) (g:=h)). unfold CoUA_eq in |- *; simpl in |- *. unfold Equal_Pmor in |- *; simpl in |- *; split. apply Refl. apply Refl. Qed.
imports: Diagonal CCC Terminal1