proposition: Theorem Cones_to_Comma `(F : [J, C]) : Cones F ⟶ (Δ ↓ =(F)).
proof: Proof. functor; simpl; intros. - exists (vertex_obj[X], ttt). transform; simpl; intros. + apply @vertex_map. exact (@coneFrom _ _ _ X). + abstract (rewrite id_right; apply cone_coherence). + abstract (rewrite id_right; symmetry; apply cone_coherence). - exists (`1 f, ttt); abstract (simpl; intros; cat). - abstract proper. - abstract cat. - abstract cat. Defined.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Functor.Diagonal Category.Structure.Cone Category.Construction.Comma Category.Instance.Cones Category.Instance.Fun Category.Instance.Cat