proposition: Lemma comp_cofipr2_cofipr_dotted : forall a u v y1 y2, has_cofiprod a u v -> cofiprod_hypothesis a u v y1 y2 -> comp a (cofipr_dotted a u v y1 y2) (cofipr2 a u v) = y2.
proof: Proof. ir. rwi has_cofipr_has_fipr H. rwi cofi_hyp_fi_hyp H0. uf cofipr_dotted. uf cofipr2. ap flip_eq. wr comp_opp. ap comp_fipr2_fipr_dotted. am. am. app mor_fipr2. app mor_fipr_dotted. rw target_fipr_dotted. tv. rw source_fipr2. tv. am. am. am. uh H0; ee. uh H1; ee; am. uh H0; ee. uh H1; ee; am. Qed.
imports: Arith colimits little_cat fc_limits cardinal