proposition: Lemma UA_isInitial : IsInitial UA_com_arrow.
proof: Proof. unfold IsInitial in |- *; intros b f. unfold UA_com_arrow in |- *; simpl in |- *; unfold Equal_com_arrow in |- *; simpl in |- *. apply UA_unic. apply Sym; apply (Prf_com_law f). Qed.
imports: Comma UniversalArrow