proposition: Lemma opp_morphisms_isomorphic : forall a, Category.axioms a -> are_isomorphic (morphisms a) (morphisms (opp a)).
proof: Proof. ir. rw iso_trans_ex_rw. sh flip. uhg; dj. uhg. ir. assert (mor a x). app is_mor_mor. change (is_mor (opp a) (flip x)). ap mor_is_mor. rw mor_opp. rww flip_flip. uhg; ee. am. uhg. ir. assert (mor (opp a) x). ap is_mor_mor. app opp_axioms. am. sh (flip x). ee. change (is_mor a (flip x)). ap mor_is_mor. wr mor_opp. am. rww flip_flip. uhg; ee. am. uhg. ir. transitivity (flip (flip x)). rww flip_flip. rw H4. rww flip_flip. Qed.
imports: Arith cat_examples cardinal fc_limits