Lemma make_PreShv_functor_z_iso (F G : functor (PreShv C) (PreShv C)) (set_iso : ∏ X c, z_iso (pr1 (F X) c) (pr1 (G X) c)) (nat_in_c : ∏ X, is_nat_trans _ _ (λ c, set_iso X c)) (nat_in_X : is_nat_trans F G (λ X, make_nat_trans _ _ _ (nat_in_c X))) : @z_iso [PreShv C, PreShv C] F G. Proof. exists (make_PreShv_functor_z_iso_helper F G set_iso nat_in_c nat_in_X). use make_is_z_isomorphism. + use make_PreShv_functor_z_iso_helper. * intros X c. exact (z_iso_inv_from_z_iso (set_iso X c)). * abstract (intros X c y f; apply pathsinv0, z_iso_inv_on_left; rewrite <- assoc; now apply pathsinv0, z_iso_inv_on_right, (nat_in_c X)). * abstract (intros X Y α; apply nat_trans_eq; [ apply homset_property|]; intro x; simpl; apply pathsinv0, (z_iso_inv_on_left _ _ _ _ (set_iso Y x)); rewrite <- assoc; apply pathsinv0, (z_iso_inv_on_right (C:=HSET)); exact (eqtohomot (maponpaths pr1 (nat_in_X X Y α)) x)). + abstract (use make_is_inverse_in_precat; [ apply nat_trans_eq; [ apply homset_property |]; intro X; apply nat_trans_eq; [ apply homset_property |]; intro x; exact (z_iso_inv_after_z_iso (set_iso X x)) | apply nat_trans_eq; [ apply homset_property |]; intro X; apply nat_trans_eq; [ apply homset_property |]; intro x; apply funextsec; intros y; exact (eqtohomot (z_iso_after_z_iso_inv (set_iso X x)) y) ]). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.LatticeObject. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.Equalizers. Require Import UniMath.CategoryTheory.Limits.PullbackConstructions.