Lemma second_iso_nat_in_F : is_nat_trans Fun1 Fun2 (λ F, make_nat_trans (pr1 (Fun1 F)) (pr1 (Fun2 F)) (second_iso_on_sets F) (second_iso_nat_in_x F)). Proof. intros X Y f. apply (nat_trans_eq has_homsets_HSET); intro. apply funextsec; intros g. apply (nat_trans_eq has_homsets_HSET); intro. apply funextsec; intros h. apply (maponpaths (pr1 f x0)). apply (maponpaths (pr1 (pr1 g x0 (pr2 h)) x0)). now apply pathsdirprod; [use id_left|]. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.YonedaBinproducts. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Categories.HSET.MonoEpiIso. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Presheaf.