Lemma third_iso_on_sets (F : PreShv C) (x : C) : z_iso (pr1 (Fun2 F) x) (pr1 (Fun3 F) x). Proof. use hset_equiv_z_iso. use iso_comp_right_weq. use iso_yoneda_binproducts. Defined.
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.