proposition: Corollary Diagonal_Unique (J C : Category) {D : Category} (d : D) : Δ[J](d) ≈[Cat] Δ(d) ∘[Cat] one.
proof: Proof. exists (fun _ => iso_id); simpl; intros; cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Diagonal Category.Structure.Terminal Category.Instance.Cat Category.Instance.One