proposition: Lemma nat_trans_inv_is_iso {C : precategory_data}{D : precategory} (hs: has_homsets D) {F G : functor_data C D} (A : nat_trans F G) (H : is_nat_iso A) : is_nat_iso (nat_trans_inv_from_pointwise_inv_ext hs A H).
proof: Proof. intros a. apply is_iso_inv_from_iso. Defined.
imports: UniMath.Foundations.Propositions UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence