proposition: Lemma are_inverse_fmor : forall a f u v, Functor.axioms f -> are_inverse (source f) u v -> target f = a -> are_inverse a (fmor f u) (fmor f v).
proof: Proof. ir. wr H1. cp H0. uh H2; ee. uh H2; uh H3; ee. uhg; ee. fw. app is_mor_mor. fw. app is_mor_mor. fw. rww H4. app is_mor_mor. app is_mor_mor. fw. rww H5. app is_mor_mor. app is_mor_mor. fw. rww comp_fmor. rww H6. fw. cw. app is_mor_mor. app is_mor_mor. app is_mor_mor. app is_mor_mor. rww comp_fmor. rww H7. fw. app is_mor_mor. cw. app is_mor_mor. app is_mor_mor. app is_mor_mor. Qed.
imports: Arith category