Description: An initial object is a terminal object in the opposite category. An alternate definition of df-inito depending on df-termo . (Contributed by Zhi Wang, 29-Aug-2024)