Commit 2023-08-18 09:50 a016a32e

View on Github →

reverting an unwanted addition to CategoryTheory.Quotient

Estimated changes

Modified Mathlib/CategoryTheory/Quotient.lean

deleted theorem CategoryTheory.Quotient.comp_natTransLift

deleted def CategoryTheory.Quotient.natIsoLift

deleted def CategoryTheory.Quotient.natTransLift

deleted theorem CategoryTheory.Quotient.natTransLift_app

deleted theorem CategoryTheory.Quotient.natTransLift_id

deleted theorem CategoryTheory.Quotient.natTrans_ext