proposition: Lemma are_finverse_umorphism_inverse : forall f g, Functor.axioms f -> Functor.axioms g -> are_finverse f g = Umorphism.are_inverse f g.
proof: Proof. ir. app iff_eq; ir. uh H1; ee. uhg; ee. uhg; ee. app functor_umorphism_axioms. app functor_umorphism_axioms. am. uhg; ee. app functor_umorphism_axioms. app functor_umorphism_axioms. am. exact H5. exact H6. uh H1; ee. uh H1; ee. uh H2; ee. uhg; ee. am. am. am. am. exact H3. exact H4. Qed.
imports: Arith category