Lemma third_iso_nat_in_F : is_nat_trans Fun2 Fun3 (λ F, make_nat_trans (pr1 (Fun2 F)) (pr1 (Fun3 F)) (third_iso_on_sets F) (third_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; apply idpath. 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.