proposition: Lemma has_fiprod_rw : forall a u v, has_fiprod a u v = (exists y1, exists y2, is_fiprod a u v y1 y2).
proof: Proof. ir. ap iff_eq; ir. uh H; ee. uh H0. nin H0. uh H0; ee. sh (fimap1 x). sh (fimap2 x). uhg; ee. ap fiprod_hypothesis_fimaps. am. app is_limit_is_cone. am. assert (is_cone x). app is_limit_is_cone. util (fiprod_cone_eq (a:=a) (u:=u) (v:=v) (c:=x)). am. am. am. wr H3. am. nin H. nin H. uhg; ee. uh H; ee. uh H; ee; am. uh H; ee. uhg. sh (fiprod_cone a u v x x0). uhg; ee. am. rww socle_fiprod_cone. Qed.
imports: Arith colimits little_cat fc_limits cardinal