Commit 2026-04-29 18:06 a3fde501

View on Github →

chore(CategoryTheory): use notation for TypeCat.ofHom (#38655) Replace uses of TypeCat.ofHom in the library by the notation ↾. Also makes the notation scoped in CategoryTheory instead of TypeCat.

Estimated changes

Modified Mathlib/Algebra/Category/AlgCat/Basic.lean

Modified Mathlib/Algebra/Category/Grp/Adjunctions.lean

Modified Mathlib/Algebra/Category/Grp/Basic.lean

Modified Mathlib/Algebra/Category/Grp/Yoneda.lean

Modified Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/LeftResolution.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/ColimitFunctor.lean

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf/Free.lean

Modified Mathlib/Algebra/Category/ModuleCat/Semi.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf.lean

Modified Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean

Modified Mathlib/Algebra/Category/MonCat/Adjunctions.lean

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

Modified Mathlib/Algebra/Category/MonCat/Yoneda.lean

Modified Mathlib/Algebra/Category/Ring/Adjunctions.lean

Modified Mathlib/Algebra/Category/Semigrp/Basic.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

modified theorem AlgebraicGeometry.Scheme.forget_map

Modified Mathlib/AlgebraicGeometry/Sites/ConstantSheaf.lean

Modified Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

Modified Mathlib/AlgebraicTopology/SimplicialNerve.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Homotopy.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Nonempty.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/PiZero.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean

Modified Mathlib/CategoryTheory/Action.lean

Modified Mathlib/CategoryTheory/Action/Concrete.lean

Modified Mathlib/CategoryTheory/Adjunction/Limits.lean

Modified Mathlib/CategoryTheory/Category/Cat.lean

Modified Mathlib/CategoryTheory/Category/Cat/Adjunction.lean

Modified Mathlib/CategoryTheory/Category/Cat/Limit.lean

Modified Mathlib/CategoryTheory/Category/Pointed.lean

Modified Mathlib/CategoryTheory/Category/RelCat.lean

Modified Mathlib/CategoryTheory/CodiscreteCategory.lean

Modified Mathlib/CategoryTheory/CofilteredSystem.lean

Modified Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Forget.lean

Modified Mathlib/CategoryTheory/Elements.lean

Modified Mathlib/CategoryTheory/Enriched/Basic.lean

Modified Mathlib/CategoryTheory/Extensive.lean

Modified Mathlib/CategoryTheory/FintypeCat.lean

modified theorem FintypeCat.id_hom

Modified Mathlib/CategoryTheory/Functor/FunctorHom.lean

Modified Mathlib/CategoryTheory/Functor/Hom.lean

Modified Mathlib/CategoryTheory/Functor/KanExtension/Dense.lean

Modified Mathlib/CategoryTheory/Galois/Prorepresentability.lean

Modified Mathlib/CategoryTheory/Galois/Topology.lean

Modified Mathlib/CategoryTheory/Generator/Type.lean

Modified Mathlib/CategoryTheory/Groupoid/Grpd/Basic.lean

Modified Mathlib/CategoryTheory/IsomorphismClasses.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

Modified Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Images.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/CategoryTheory/Limits/IsLimit.lean

Modified Mathlib/CategoryTheory/Limits/MonoCoprod.lean

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

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

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

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

Modified Mathlib/CategoryTheory/Limits/Types/Coequalizers.lean

Modified Mathlib/CategoryTheory/Limits/Types/Colimits.lean

Modified Mathlib/CategoryTheory/Limits/Types/Coproducts.lean

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

Modified Mathlib/CategoryTheory/Limits/Types/Filtered.lean

Modified Mathlib/CategoryTheory/Limits/Types/Images.lean

Modified Mathlib/CategoryTheory/Limits/Types/Limits.lean

Modified Mathlib/CategoryTheory/Limits/Types/Products.lean

Modified Mathlib/CategoryTheory/Limits/Types/Pullbacks.lean

Modified Mathlib/CategoryTheory/Limits/Types/Pushouts.lean

modified def CategoryTheory.Limits.Types.Pushout.inl

modified def CategoryTheory.Limits.Types.Pushout.inr

Modified Mathlib/CategoryTheory/Limits/Types/Yoneda.lean

Modified Mathlib/CategoryTheory/Limits/Yoneda.lean

Modified Mathlib/CategoryTheory/Monad/Types.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided/Reflection.lean

Modified Mathlib/CategoryTheory/Monoidal/Closed/FunctorToTypes.lean

Modified Mathlib/CategoryTheory/Monoidal/Closed/Types.lean

Modified Mathlib/CategoryTheory/Monoidal/Functor/Types.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp.lean

Modified Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Concrete.lean

Modified Mathlib/CategoryTheory/Preadditive/Injective/Basic.lean

Modified Mathlib/CategoryTheory/Preadditive/Projective/Basic.lean

Modified Mathlib/CategoryTheory/Presentable/Type.lean

Modified Mathlib/CategoryTheory/ShrinkYoneda.lean

Modified Mathlib/CategoryTheory/Sites/Closed.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean

Modified Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean

Modified Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean

Modified Mathlib/CategoryTheory/Sites/GlobalSections.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

Modified Mathlib/CategoryTheory/Sites/Preserves.lean

Modified Mathlib/CategoryTheory/Sites/Sheaf.lean

Modified Mathlib/CategoryTheory/Sites/SheafHom.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/Sites/Subcanonical.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Sites/Types.lean

Modified Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean

Modified Mathlib/CategoryTheory/Subfunctor/Basic.lean

modified def CategoryTheory.Subfunctor.ι

Modified Mathlib/CategoryTheory/Subfunctor/Image.lean

Modified Mathlib/CategoryTheory/Subobject/Lattice.lean

Modified Mathlib/CategoryTheory/Subobject/Presheaf.lean

Modified Mathlib/CategoryTheory/Subobject/Types.lean

modified theorem subtype_val_mono

Modified Mathlib/CategoryTheory/Topos/Sheaf.lean

Modified Mathlib/CategoryTheory/Types/Basic.lean

Modified Mathlib/CategoryTheory/Types/Set.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

Modified Mathlib/Combinatorics/Hall/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean

Modified Mathlib/Combinatorics/SimpleGraph/Finsubgraph.lean

Modified Mathlib/Condensed/Discrete/Colimit.lean

Modified Mathlib/Condensed/Discrete/LocallyConstant.lean

Modified Mathlib/Condensed/Light/Functors.lean

Modified Mathlib/Condensed/Light/TopCatAdjunction.lean

Modified Mathlib/Condensed/TopCatAdjunction.lean

Modified Mathlib/Condensed/TopComparison.lean

Modified Mathlib/Control/Fold.lean

Modified Mathlib/Geometry/Manifold/Sheaf/Smooth.lean

Modified Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

Modified Mathlib/RepresentationTheory/Homological/Resolution.lean

Modified Mathlib/RingTheory/Invariant/Profinite.lean

Modified Mathlib/Topology/Category/CompHausLike/SigmaComparison.lean

Modified Mathlib/Topology/Category/Compactum.lean

Modified Mathlib/Topology/Category/LightProfinite/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Basic.lean

Modified Mathlib/Topology/Category/Profinite/Extend.lean

Modified Mathlib/Topology/Category/TopCat/Yoneda.lean

Modified Mathlib/Topology/Homotopy/Lifting.lean

Modified Mathlib/Topology/Sheaves/LocalPredicate.lean

modified def TopCat.subpresheafToTypes.subtype

Modified Mathlib/Topology/Sheaves/Points.lean

Modified Mathlib/Topology/Sheaves/PresheafOfFunctions.lean

Modified Mathlib/Topology/Sheaves/Sheafify.lean