Lemma ConeConnect_idtoiso (M N : CONE F) (p : M = N): ConeConnect _ _ _ (pr1 (idtoiso p)) = idtoiso ((base_paths _ _ (base_paths _ _ p))). Proof. destruct p. 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.