proposition: 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: 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.
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