proposition: Lemma z_iso_Universal_weq {C:category} {X Y:[C^op,HSET]} (c:C) : z_iso X Y -> Universal X c ≃ Universal Y c.
proof: Proof. intro i. set (I := (functor_z_iso_pointwise_if_z_iso C^op HSET (homset_property HSET) X Y (pr1 i) (pr2 i))). unshelve refine (weqbandf _ _ _ _). - apply hset_z_iso_equiv_weq. unfold arrow, functor_object_application. exact (I c). - simpl; intros x. apply weqonsecfibers; intro b. apply weqiff. + unshelve refine (twooutof3c_iff_1_homot _ _ _ _ _). * exact (pr1 i ◽ opp_ob b). * intro f; simpl. exact (eqtohomot (nat_trans_ax (pr1 i) _ _ f) x). * exact (hset_z_iso_is_equiv _ _ (I b)). + apply isapropisweq. + apply isapropisweq. Defined.
imports: UniMath.Foundations.Preamble UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.MonoEpiIso UniMath.CategoryTheory.RepresentableFunctors.Bifunctor UniMath.CategoryTheory.RepresentableFunctors.Precategories UniMath.MoreFoundations.Tactics