fact: Definition Δ {C J : Category} := @Diagonal C J.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Natural.Transformation Category.Construction.Product Category.Instance.Fun Category.Instance.One