proposition: Lemma Prf_eq2_prod1 : Eq2_prod_law Proj2_prod1 Op_together1.
proof: Proof. unfold Eq2_prod_law in |- *; intros c f g. unfold Together_prod, Op_together1, Together1, Proj2_prod1, Ap2 in |- *; simpl in |- *. generalize (Prf_isCoUA_law1 ua' (Build_Pmor (u:=Build_POb c c) (t:=Build_POb a b) f g)). unfold CoUA_eq in |- *; simpl in |- *. unfold Equal_Pmor in |- *; simpl in |- *. simple induction 1. intros H2 H3. apply H3. Qed.
imports: Diagonal CCC Terminal1