proposition: Lemma equalizer_hypothesis_eqzmap : forall a u v c, twoarrow_hypothesis a u v -> is_cone c -> socle c = twoarrow_functor a u v -> equalizer_hypothesis a u v (eqzmap c).
proof: Proof. ir. assert (a = cone_target c). uf cone_target. rw H1. rw target_twoarrow_functor. tv. assert (cone_source c = twoarrow_cat). uf cone_source. rw H1. rww source_twoarrow_functor. uhg. ee. am. uf eqzmap. rw H2. ap mor_edge. rw H3. ap ob_twoarrow_cat. am. uf eqzmap. rw target_edge. rw H1. rw fob_twoarrow_functor_R. tv. am. rw H3. ap ob_twoarrow_cat. am. set (k:= edge_nt c). util (twoarrow_nt_ntrans (u:=k)). uf k. app edge_nt_axioms. uf k. rww osource_edge_nt. assert (otarget k = a). uf k. rww otarget_edge_nt. sy; am. assert (fmor (source k) (catyd_arrow (d:=twoarrow_data) a0') = id a (vertex c)). uf k. rw source_edge_nt. rw fmor_constant_functor. wr H2. tv. rw H3. ap mor_twoarrow_cat. am. assert (fmor (source k) (catyd_arrow (d:=twoarrow_data) a1') = id a (vertex c)). uf k. rw source_edge_nt. rw fmor_constant_functor. wr H2. tv. rw H3. ap mor_twoarrow_cat. am. assert (fmor (target k) (catyd_arrow (d:=twoarrow_data) a0') = u). uf k. rw target_edge_nt. rw H1. rw fmor_twoarrow_functor_catyd_arrow. tv. am. assert (fmor (target k) (catyd_arrow (d:=twoarrow_data) a1') = v). uf k. rw target_edge_nt. rw H1. rw fmor_twoarrow_functor_catyd_arrow. tv. am. util (twoarrow_nt_hypothesis_ntrans (u:=k)). uf k. app edge_nt_axioms. uf k. rw osource_edge_nt. am. am. rwi H6 H10. rwi H5 H10. rwi H7 H10. rwi H8 H10. rwi H9 H10. assert (ntrans k (R o1') = eqzmap c). uf eqzmap. uf edge. tv. rwi H11 H10. set (m:= ntrans k (R o2')). assert (m = ntrans k (R o2')). tv. wri H12 H10. uh H10; ee. wr H27. wr H28. reflexivity. Qed.
imports: Arith colimits little_cat fc_limits cardinal