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`.

Author: dagurtomas

Mathlib/Algebra/Category/AlgCat/Basic.lean

@@ -192,7 +192,7 @@ set_option backward.isDefEq.respectTransparency false in
 def adj : free.{u} R ⊣ forget (AlgCat.{u} R) :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun _ _ =>
-        { toFun := fun f ↦ TypeCat.ofHom ((FreeAlgebra.lift _).symm f.hom)
+        { toFun := fun f ↦ ↾((FreeAlgebra.lift _).symm f.hom)
           invFun := fun f ↦ ofHom <| (FreeAlgebra.lift _) f
           left_inv := fun f ↦ by aesop
           right_inv := fun f ↦ by aesop } }
@@ -229,8 +229,8 @@ end CategoryTheory.Iso
 @[simps]
 def algEquivIsoAlgebraIso {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] :
     (X ≃ₐ[R] Y) ≅ (AlgCat.of R X ≅ AlgCat.of R Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toAlgebraIso)
-  inv := TypeCat.ofHom (fun i ↦ i.toAlgEquiv)
+  hom := ↾fun e ↦ e.toAlgebraIso
+  inv := ↾fun i ↦ i.toAlgEquiv
 
 instance AlgCat.forget_reflects_isos : (forget (AlgCat.{u} R)).ReflectsIsomorphisms where
   reflects {X Y} f _ := by

Mathlib/Algebra/Category/Grp/Adjunctions.lean

@@ -104,7 +104,7 @@ instance : (free.{u}).PreservesMonomorphisms where
         ((Types.initial_iff_empty X).2 hX).some).isZero.eq_of_tgt
     · have hf : Function.Injective f := by rwa [← mono_iff_injective]
       obtain ⟨g, hg⟩ := hf.hasLeftInverse
-      have : IsSplitMono f := IsSplitMono.mk' { retraction := TypeCat.ofHom g }
+      have : IsSplitMono f := IsSplitMono.mk' { retraction := ↾g }
       infer_instance
 
 end AddCommGrpCat

Mathlib/Algebra/Category/Grp/Basic.lean

@@ -544,8 +544,8 @@ end CategoryTheory.Iso
 in `GrpCat` -/
 @[to_additive]
 def mulEquivIsoGroupIso {X Y : GrpCat.{u}} : (X ≃* Y) ≅ (X ≅ Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toGrpIso)
-  inv := TypeCat.ofHom (fun i ↦ i.groupIsoToMulEquiv)
+  hom := ↾fun e ↦ e.toGrpIso
+  inv := ↾fun i ↦ i.groupIsoToMulEquiv
 
 /-- Additive equivalences between `AddGroup`s are the same
 as (isomorphic to) isomorphisms in `AddGrpCat`. -/
@@ -555,8 +555,8 @@ add_decl_doc addEquivIsoAddGroupIso
 in `CommGrpCat`. -/
 @[to_additive]
 def mulEquivIsoCommGroupIso {X Y : CommGrpCat.{u}} : (X ≃* Y) ≅ (X ≅ Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toCommGrpIso)
-  inv := TypeCat.ofHom (fun i ↦ i.commGroupIsoToMulEquiv)
+  hom := ↾fun e ↦ e.toCommGrpIso
+  inv := ↾fun i ↦ i.commGroupIsoToMulEquiv
 
 /-- Additive equivalences between `AddCommGroup`s are
 the same as (isomorphic to) isomorphisms in `AddCommGrpCat`. -/

Mathlib/Algebra/Category/Grp/Yoneda.lean

@@ -35,8 +35,8 @@ coyoneda embedding. -/]
 def CommGrpCat.coyonedaForget :
     coyoneda ⋙ (Functor.whiskeringRight _ _ _).obj (forget _) ≅ CategoryTheory.coyoneda :=
   dsimp% NatIso.ofComponents fun X ↦ NatIso.ofComponents fun Y ↦ {
-    hom := TypeCat.ofHom (fun f ↦ ofHom f),
-    inv := TypeCat.ofHom (fun f ↦ f.hom) }
+    hom := ↾fun f ↦ ofHom f,
+    inv := ↾fun f ↦ f.hom }
 
 /-- The Hom bifunctor sending a type `X` and a commutative group `G` to the commutative group
 `X → G` with pointwise operations.

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -75,8 +75,8 @@ lemma free_map_apply {X Y : Type u} (f : X ⟶ Y) (x : X) :
 @[simps]
 def freeHomEquiv {X : Type u} {M : ModuleCat.{u} R} :
     ((free R).obj X ⟶ M) ≃ (X ⟶ M) where
-  toFun φ := TypeCat.ofHom (fun x ↦ φ (freeMk x))
-  invFun ψ := freeDesc (TypeCat.ofHom ψ)
+  toFun φ := ↾fun x ↦ φ (freeMk x)
+  invFun ψ := freeDesc (↾ψ)
   left_inv _ := by ext; simp
   right_inv _ := by ext; simp
 

Mathlib/Algebra/Category/ModuleCat/Basic.lean

@@ -299,8 +299,8 @@ in `ModuleCat` -/
 @[simps]
 def linearEquivIsoModuleIso {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module R X]
     [Module R Y] : (X ≃ₗ[R] Y) ≅ (ModuleCat.of R X ≅ ModuleCat.of R Y) where
-  hom := TypeCat.ofHom (fun e ↦ e.toModuleIso)
-  inv := TypeCat.ofHom (fun i ↦ i.toLinearEquiv)
+  hom := ↾fun e ↦ e.toModuleIso
+  inv := ↾fun i ↦ i.toLinearEquiv
 
 end
 

Mathlib/Algebra/Category/ModuleCat/LeftResolution.lean

@@ -34,7 +34,7 @@ instance (X : Type u) : Projective ((free R).obj X) where
   factors {M N} f p hp := by
     rw [epi_iff_surjective] at hp
     obtain ⟨s, hs⟩ := hp.hasRightInverse
-    exact ⟨freeDesc (TypeCat.ofHom (fun x ↦ s (f (freeMk x)))), by cat_disch⟩
+    exact ⟨freeDesc (↾fun x ↦ s (f (freeMk x))), by cat_disch⟩
 
 set_option backward.isDefEq.respectTransparency false in
 /-- An `R`-module `M` can be functorially written as a quotient of a

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

@@ -79,7 +79,7 @@ by `cR.pt` on `ModuleColimit hcR hcM`. -/
 noncomputable def coconeSMul :
     Cocone (R ⋙ forget _ ⊗ M.presheaf ⋙ forget _) where
   pt := ModuleColimit hcR hcM
-  ι.app U := TypeCat.ofHom fun ⟨(r : R.obj U), (m : M.obj U)⟩ ↦ by exact cM.ι.app U (r • m)
+  ι.app U := ↾fun ⟨(r : R.obj U), (m : M.obj U)⟩ ↦ by exact cM.ι.app U (r • m)
   ι.naturality V U f := by
     ext ⟨r, m⟩
     exact (ConcreteCategory.congr_arg (cM.ι.app U)

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

@@ -41,7 +41,7 @@ of modules over `R` which sends `X : Cᵒᵖ` to the free `R.obj X`-module on `F
 @[simps]
 noncomputable def freeObj (F : Cᵒᵖ ⥤ Type u) : PresheafOfModules.{u} R where
   obj X := (ModuleCat.free (R.obj X)).obj (F.obj X)
-  map {X Y} f := ModuleCat.freeDesc (TypeCat.ofHom (fun x ↦ ModuleCat.freeMk (F.map f x)))
+  map {X Y} f := ModuleCat.freeDesc (↾fun x ↦ ModuleCat.freeMk (F.map f x))
   map_id := by aesop
 
 /-- The free presheaf of modules functor `(Cᵒᵖ ⥤ Type u) ⥤ PresheafOfModules.{u} R`. -/
@@ -71,7 +71,7 @@ variable (F R) in
 /-- The unit of `PresheafOfModules.freeAdjunction`. -/
 @[simps]
 noncomputable def freeAdjunctionUnit : F ⟶ (freeObj (R := R) F).presheaf ⋙ forget _ where
-  app X := TypeCat.ofHom (fun x ↦ ModuleCat.freeMk x)
+  app X := ↾fun x ↦ ModuleCat.freeMk x
   naturality X Y f := by ext; simp [presheaf]
 
 set_option backward.isDefEq.respectTransparency false in

Mathlib/Algebra/Category/ModuleCat/Semi.lean

@@ -273,8 +273,8 @@ in `SemimoduleCat` -/
 def linearEquivIsoModuleIsoₛ {X Y : Type u} [AddCommMonoid X] [AddCommMonoid Y] [Module R X]
     [Module R Y] : (X ≃ₗ[R] Y) ≅
       ((SemimoduleCat.of R X) ≅ (SemimoduleCat.of R Y)) where
-  hom := TypeCat.ofHom (fun e ↦ e.toModuleIsoₛ)
-  inv := TypeCat.ofHom (fun i ↦ i.toLinearEquivₛ)
+  hom := ↾fun e ↦ e.toModuleIsoₛ
+  inv := ↾fun i ↦ i.toLinearEquivₛ
 
 end