Lemma base_paths_isotoid_CONE (M : CONE F): base_paths (pr1 M) (pr1 M) (base_paths M M (isotoid_CONE (identity_z_iso M))) = base_paths (pr1 M) (pr1 M) (idpath (pr1 M)). Proof. intermediate_path (base_paths (pr1 M) (pr1 M) (isotoid_CONE_pr1 M M (identity_z_iso M))). unfold Cone_eq. apply maponpaths. apply base_total2_paths. intermediate_path (isotoid C is_cat_C (ConeConnectIso _ _ _ (identity_z_iso M))). unfold isotoid_CONE_pr1. apply base_total2_paths. intermediate_path (isotoid C is_cat_C (identity_z_iso (ConeTop _ _ _ (pr1 M)))). apply maponpaths, ConeConnectIso_identity_iso. apply isotoid_identity_iso. 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.