proposition: Lemma has_eq_has_coeq : forall a u v, Category.axioms a -> has_equalizer a u v = has_coequalizer (opp a) (flip u) (flip v).
proof: Proof. ir. rw has_coeq_has_eq. rw flip_flip. rw flip_flip. rw opp_opp. tv. app opp_axioms. Qed.
imports: Arith colimits little_cat fc_limits cardinal