fact: Definition twoarrow_nt_hypothesis a u1 v1 u2 v2 r s:= Category.axioms a & mor a u1 & mor a v1 & mor a u2 & mor a v2 & mor a r & mor a s & source r = source u1 & target r = source u2 & source s = target u1 & target s = target u2 & source u1 = source v1 & target u1 = target v1 & source u2 = source v2 & target u2 = target v2 & comp a s u1 = comp a u2 r & comp a s v1 = comp a v2 r.
imports: Arith cat_examples cardinal fc_limits