proposition: Lemma fimaps_extensionality : forall a b, is_cone a -> is_cone b -> cone_source a = vee_cat -> socle a = socle b -> fimap1 a = fimap1 b -> fimap2 a = fimap2 b -> a = b.
proof: Proof. ir. assert (cone_source b = vee_cat). uf cone_source. wr H2. am. util (fiprod_cone_eq2 (c:= a)). am. am. util (fiprod_cone_eq2 (c:= b)). am. am. rw H6; rw H7. assert (veefirst a = veefirst b). uf veefirst. rww H2. assert (veesecond a = veesecond b). uf veesecond. rw H2. reflexivity. rw H3; rw H8; rw H9. assert (cone_target a = cone_target b). uf cone_target. rww H2. rw H10. rw H4. reflexivity. Qed.
imports: Arith colimits little_cat fc_limits cardinal