proposition: 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: 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.
imports: UniMath.MoreFoundations.All UniMath.Algebra.Monoids UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Monics UniMath.CategoryTheory.LatticeObject UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Pullbacks