Commit 2023-04-27 15:27 1a35e03b

View on Github →

feat: port CategoryTheory.Sites.Adjunction (#3663)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Adjunction.lean

added def CategoryTheory.Sheaf.adjunction

added def CategoryTheory.Sheaf.adjunctionToTypes

added theorem CategoryTheory.Sheaf.adjunctionToTypes_counit_app_val

added theorem CategoryTheory.Sheaf.adjunctionToTypes_unit_app_val

added def CategoryTheory.Sheaf.composeEquiv