proposition: Lemma fmor_inverse : forall a f u, Functor.axioms f -> invertible (source f) u -> source f = a -> fmor f (inverse a u) = inverse (target f) (fmor f u).
proof: Proof. ir. ap inverse_uni. sh (target f). sh (fmor f u). ee. app are_inverse_fmor. rw H1. app invertible_inverse. wrr H1. app invertible_inverse. app invertible_fmor. Qed.
imports: Arith category