Generator of Type

In this file, we show that PUnit is a separator of the category Type u.

theorem CategoryTheory.Types.isSeparator_punit : IsSeparator PUnit.{u + 1}