proposition: Lemma equalizer_hypothesis_eqz : forall c, is_cone c -> cone_source c = twoarrow_cat -> equalizer_hypothesis (cone_target c) (eqzfirst c) (eqzsecond c) (eqzmap c).
proof: Proof. ir. util (equalizer_hypothesis_eqzmap (a:= cone_target c) (u:= eqzfirst c) (v:= eqzsecond c) (c:=c)). uf eqzfirst. uf eqzsecond. uf cone_target. ap functor_twoarrow_hypothesis. app socle_axioms. am. am. uf cone_target. uf eqzfirst. uf eqzsecond. ap functor_twoarrow_eq. app socle_axioms. am. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal