proposition: Lemma Cone_Comma `(F : [J, C]) : (Δ ↓ Δ(F)) ↔ Cone F.
proof: Proof. split; simpl. - intros [[? ?] f]. simplify; simpl in *. unshelve econstructor; [ exact o | unshelve econstructor ]. + now apply f. + abstract(destruct f; simpl in *; intros x y f; rewrite <- (id_right (transform y)); now apply naturality). - intros X. destruct X. exists (vertex_obj, vertex_obj). construct. + now apply vertex_map. + abstract(simpl; rewrite id_right; now apply cone_coherence). + abstract(simpl; rewrite id_right; symmetry; now apply cone_coherence). Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Diagonal Category.Structure.Cone Category.Construction.Comma Category.Instance.Fun