proposition: Lemma id_weq_z_iso_slicecat (af bg : C / x) : (af = bg) ≃ (z_iso af bg).
proof: 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.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Epis