proposition: Lemma Cone_Natural_Transform `(F : [J, C]) : ∀ N : C, Δ[J](N) ⟹ F ↔ Cone[N] F.
proof: Proof. split; intros. - construct; [ exact (X x) |]. abstract(pose proof (naturality[X] _ _ f) as nat; simpl in nat; rewrite id_right in nat; now apply nat). - construct. + now apply X. + abstract(simpl; rewrite id_right; apply cone_coherence). + abstract(simpl; rewrite id_right; symmetry; 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