Definition isotoid_CONE_pr1 (a b : CONE F) : z_iso a b -> pr1 a = pr1 b. Proof. intro f. apply (total2_paths_f (isotoid _ is_cat_C (ConeConnectIso _ _ _ f))). intermediate_path ((λ c : J, idtoiso (!isotoid C is_cat_C (ConeConnectIso _ _ _ f))· pr2 (pr1 a) c)). apply transportf_isotoid_dep'. apply funextsec. intro t. intermediate_path (idtoiso (isotoid C is_cat_C (z_iso_inv_from_z_iso (ConeConnectIso _ _ _ f)))· pr2 (pr1 a) t). apply cancel_postcomposition. apply maponpaths. apply maponpaths. apply inv_isotoid. intermediate_path (z_iso_inv_from_z_iso (ConeConnectIso _ _ _ f)· pr2 (pr1 a) t). apply cancel_postcomposition. set (H := idtoiso_isotoid _ is_cat_C _ _ (z_iso_inv_from_z_iso (ConeConnectIso _ _ _ f))). simpl in *. apply (base_paths _ _ H). simpl. set (T':= inv_from_z_iso f). set (T:=pr2 (inv_from_z_iso f) t). simpl in *. rewrite <- inv_from_iso_ConeConnectIso. apply T. Defined.
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.