FintypeCat.hom_ext

theorem FintypeCat.hom_ext : ∀ {X Y : FintypeCat} (f g : X ⟶ Y), (∀ (x : ↑X), f x = g x) → f = g

This theorem states that for any two objects `X` and `Y` in the category of finite types (`FintypeCat`), if two morphisms (functions) `f` and `g` from `X` to `Y` are such that their output is the same for every element of `X` (i.e., `f x = g x` for all `x` in `X`), then `f` and `g` are the same morphism. In other words, in the category of finite types, if two functions have the same effect on all elements of their domain, they are considered identical.

More concisely: In the category of finite types, two morphisms between objects are equal if and only if they map every element of their domain to the same image.