Commit 2023-09-18 13:50 3e44bb07

View on Github →

chore: replace ConeMorphism.Hom by ConeMorphism.hom (#7176)

Estimated changes

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Product.lean

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/Limits/ColimitLimit.lean

Modified Mathlib/CategoryTheory/Limits/ConeCategory.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

modified theorem CategoryTheory.Limits.CoconeMorphism.ext

modified theorem CategoryTheory.Limits.Cocones.cocone_iso_of_hom_iso

modified theorem CategoryTheory.Limits.ConeMorphism.ext

modified theorem CategoryTheory.Limits.Cones.cone_iso_of_hom_iso

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

Modified Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean

Modified Mathlib/CategoryTheory/Limits/Final.lean

Modified Mathlib/CategoryTheory/Limits/Fubini.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

modified def CategoryTheory.Limits.IsColimit.descCoconeMorphism

modified def CategoryTheory.Limits.IsLimit.liftConeMorphism

Modified Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean

modified theorem CategoryTheory.Limits.Fork.hom_comp_ι

modified theorem CategoryTheory.Limits.Fork.π_comp_hom

Modified Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

modified theorem CategoryTheory.Limits.Multicofork.π_comp_hom

modified theorem CategoryTheory.Limits.Multifork.hom_comp_ι

Modified Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean

Modified Mathlib/CategoryTheory/Sites/CompatiblePlus.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean

Modified Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean