Lemma functor_on_is_iso_is_iso {C C' : precategory} (F : functor C C') {a b : ob C} {f : a --> b} (H : is_iso f) : is_iso (#F f). Proof. apply (is_iso_qinv _ (#F (inv_from_iso (make_iso _ H)))). apply (is_inverse_functor_image _ _ _ _ _ (make_iso _ H)). Qed.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.TransportMorphisms. Require Import UniMath.CategoryTheory.Core.Univalence.