Lemma isaset_Cone_Mor (M N : Cone) : isaset (Cone_Mor M N). Proof. apply (isofhleveltotal2 2). apply C. intros. apply hlevelntosn. apply impred. intros. apply C. 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.