Lemma id_weq_z_iso_slicecat (af bg : C / x) : (af = bg) ≃ (z_iso af bg). Proof. set (a := pr1 af); set (f := pr2 af); set (b := pr1 bg); set (g := pr2 bg). assert (weq1 : weq (af = bg) (total2 (fun (p : a = b) => transportf _ p (pr2 af) = g))). { apply (total2_paths_equiv _ af bg). } assert (weq2 : weq (total2 (fun (p : a = b) => transportf _ p (pr2 af) = g)) (total2 (fun (p : a = b) => idtoiso (! p) · f = g))). { apply weqfibtototal; intro p. rewrite idtoiso_precompose. apply idweq. } assert (weq3 : weq (total2 (fun (p : a = b) => idtoiso (! p) · f = g)) (total2 (λ h : z_iso a b, f = h · g))). { apply (weqbandf (make_weq _ (is_catC a b))); intro p. rewrite idtoiso_inv; simpl. apply weqimplimpl; simpl; try apply (C); intro Hp. rewrite <- Hp, assoc, z_iso_inv_after_z_iso, id_left; apply idpath. rewrite Hp, assoc, z_iso_after_z_iso_inv, id_left; apply idpath. } assert (weq4 : weq (total2 (λ h : z_iso a b, f = h · g)) (z_iso af bg)). { apply invweq; apply weq_z_iso. } apply (weqcomp weq1 (weqcomp weq2 (weqcomp weq3 weq4))). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.Univalence. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Pullbacks. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Monics. Require Import UniMath.CategoryTheory.Epis.