proposition: Lemma inverse_fmor : forall a f u, Functor.axioms f -> invertible (source f) u -> target f = a -> inverse a (fmor f u) = fmor f (inverse (source f) u).
proof: Proof. ir. wr H1. rww fmor_inverse. Qed.
imports: Arith category