Lemma third_iso_nat_in_x (F : PreShv C) : is_nat_trans (pr1 (Fun2 F)) (pr1 (Fun3 F)) (λ x, third_iso_on_sets F x). Proof. intros X Y f. apply funextsec; intro g. apply (nat_trans_eq has_homsets_HSET); intros x. apply funextsec; intros y. apply (maponpaths (pr1 g x)), pathsdirprod; cbn; unfold yoneda_morphisms_data, BinProduct_of_functors_mor; cbn. - now rewrite <- assoc, (BinProductOfArrowsPr1 _ (PC c X) (PC c Y)), id_right. - now rewrite <- !assoc, (BinProductOfArrowsPr2 _ (PC c X) (PC c Y)). 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.