proposition: Lemma target_cofipr2 : forall a u v, has_cofiprod a u v -> target (cofipr2 a u v) = target (cofipr1 a u v).
proof: Proof. ir. cp (cofiprod_hypothesis_cofiprod H). uh H0; ee. uh H0; ee. transitivity (target (comp a (cofipr1 a u v) u)). rw H5. rw target_comp. tv. ap mor_cofipr2. am. am. rw source_cofipr2. tv. am. rw target_comp. tv. app mor_cofipr1. am. rww source_cofipr1. Qed.
imports: Arith colimits little_cat fc_limits cardinal