Lemma weq_z_iso (af bg : x / C) : z_iso af bg ≃ ∑ h : z_iso (pr1 af) (pr1 bg), pr2 af · h = pr2 bg. Proof. apply (weqcomp (weqtotal2asstor _ _)). apply invweq. apply (weqcomp (weqtotal2asstor _ _)). apply weqfibtototal; intro h; simpl. apply (weqcomp (weqdirprodcomm _ _)). apply weqfibtototal; intro p. apply weqimplimpl. - intro hp; apply z_iso_to_coslice_precat_z_iso; assumption. - intro hp; apply (coslice_precat_z_iso_to_z_iso _ _ _ hp). - apply isaprop_is_z_isomorphism. - apply (isaprop_is_z_isomorphism(C:= x / C)). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total.