proposition: Lemma idtoiso_isotoid_CONE (M N : CONE F) : ∏ f : z_iso M N, idtoiso (isotoid_CONE f) = f.
proof: Proof. intro f. apply z_iso_eq. apply Cone_Mor_eq. etrans; [apply ConeConnect_idtoiso |]. unfold isotoid_CONE. unfold Cone_eq. rewrite base_total2_paths. unfold isotoid_CONE_pr1. rewrite base_total2_paths. simpl. rewrite idtoiso_isotoid. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.MoreFoundations.PartA UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors