proposition: Lemma vee_hypothesis_opp_flip : forall a u v, Category.axioms a -> vee_hypothesis (opp a) (flip u) (flip v) = covee_hypothesis a u v.
proof: Proof. ir. transitivity (covee_hypothesis (opp (opp a)) u v). rw covee_hypothesis_opp. tv. app opp_axioms. rww opp_opp. Qed.
imports: Arith colimits little_cat fc_limits cardinal