CategoryTheory.Functor.empty_ext'

theorem CategoryTheory.Functor.empty_ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor (CategoryTheory.Discrete PEmpty.{w + 1}) C), F = G

This theorem states that any two functors originating from an empty category are equal. It is applicable to any category `C`, and to any two functors `F` and `G` that map from the empty category (represented by `CategoryTheory.Discrete PEmpty.{w + 1}`) to `C`. Note however, that in most cases, you would want to use the `emptyExt` theorem instead of this one.

More concisely: For any category `C`, any two functors from the empty category to `C` are equal.