Commit 2025-05-13 20:30 22030a26
View on Github →feat(CategoryTheory/Limits/Final): fromPUnit c is final if c is terminal (#24847)
Given an object of a category c, the functor fromPUnit c is final if the object is terminal. Dually, we show that fromPUnit c is initial when the object is initial.