proposition: Theorem Cones_from_Comma `(F : [J, C]) : (Δ ↓ =(F)) ⟶ Cones F.
proof: Proof. functor; simpl; intros. - construct; simpl; intros. + exact (fst ``X). + exists (transform[`2 X]). abstract (intros; rewrite (naturality[`2 X]); cat). - destruct f; simpl in *. exists (fst x0); abstract (intros; rewrite e; 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