Lemma idtoiso_isotoid_CONE (M N : CONE F) : ∏ f : z_iso M N, idtoiso (isotoid_CONE f) = f. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors.