Commit 2023-08-01 08:16 6965a5a6

View on Github →

feat: generalize universes for connected categories (#6237)

Estimated changes

Modified Mathlib/CategoryTheory/IsConnected.lean

modified theorem CategoryTheory.any_functor_const_on_obj

modified theorem CategoryTheory.constant_of_preserves_morphisms

modified theorem CategoryTheory.isConnected_of_equivalent

modified theorem CategoryTheory.isPreconnected_of_equivalent

modified def CategoryTheory.isoConstant

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.apply_invFun_apply