proposition: Theorem Cones_Comma `(F : [J, C]) : Cones F ≅[Cat] (Δ ↓ =(F)).
proof: Proof. isomorphism; simpl; intros. - apply Cones_to_Comma. - apply Cones_from_Comma. - constructive. + exists (id, ttt); abstract cat. + exists (id, ttt); abstract cat. + abstract (simpl; cat). + abstract (simpl; cat). + abstract (simpl; cat). - constructive. + exists id; abstract (intros; cat). + exists id; abstract (intros; cat). + abstract (simpl; cat). + abstract (simpl; cat). + abstract (simpl; cat). Qed.
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