fact: Definition fiprod_hypothesis a u v y1 y2 := vee_hypothesis a u v & mor a y1 & mor a y2 & source u = target y1 & source v = target y2 & source y1 = source y2 & comp a u y1 = comp a v y2.
imports: Arith colimits little_cat fc_limits cardinal