Definition cone {I C:category} (c:C) (D: [I,C]) : UU := ∑ (φ : ∏ i, Hom C c (D ◾ i)), ∏ i j (e : i --> j), D ▭ e ∘ φ i = φ j.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import Require Import Require Import UniMath.MoreFoundations.Tactics.