proposition: Lemma invertible_fmor : forall a f u, Functor.axioms f -> invertible (source f) u -> target f = a -> invertible a (fmor f u).
proof: Proof. ir. wr H1. uhg. uh H0. nin H0. sh (fmor f x). app are_inverse_fmor. Qed.
imports: Arith category