Lemma is_univalent_CONE : is_univalent (CONE F). Proof. intros a b. apply (isweq_iso _ (@isotoid_CONE a b)). apply isotoid_CONE_idtoiso. apply idtoiso_isotoid_CONE. 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.