Commit 2023-02-21 19:14 6d161956

View on Github →

feat: port/CategoryTheory.PUnit (#2367)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/PUnit.lean

added def CategoryTheory.Functor.equiv

added def CategoryTheory.Functor.pUnitExt

added theorem CategoryTheory.Functor.pUnit_ext'

added def CategoryTheory.Functor.star

added theorem CategoryTheory.equiv_pUnit_iff_unique