proposition: Lemma twoarrow_hypothesis_opp : forall a u v, Category.axioms a -> twoarrow_hypothesis (opp a) u v = twoarrow_hypothesis a (flip u) (flip v).
proof: Proof. ir. ap iff_eq; ir. uh H0; uhg; ee. rwi mor_opp H0. am. wrr mor_opp. rw source_flip; try alike. rw source_flip; try alike. am. rw target_flip; try alike. rw target_flip; try alike. am. uh H0; ee. wri mor_opp H0. wri mor_opp H1. uhg; ee; try am. rwi target_flip H3; try alike. rwi target_flip H3; try alike. am. rwi source_flip H2; try alike. rwi source_flip H2; try alike. am. Qed.
imports: Arith colimits little_cat fc_limits cardinal