Lemma eq_z_iso_coslicecat (af bg : x / C) (f g : z_iso af bg) : pr1 f = pr1 g -> f = g. Proof. induction f as [f fP]; induction g as [g gP]; intro eq. use (subtypePairEquality _ eq). intro; apply isaprop_is_z_isomorphism. Qed.
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.