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. 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.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.