Loogle!

Result

Found 217 declarations mentioning CategoryTheory.Cat.of. Of these, only the first 200 are shown.

• CategoryTheory.Cat.of 📋 Mathlib.CategoryTheory.Category.Cat
  (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Cat
• CategoryTheory.Cat.coe_of 📋 Mathlib.CategoryTheory.Category.Cat
  (C : CategoryTheory.Cat) : CategoryTheory.Cat.of ↑C = C
• CategoryTheory.Cat.of_α 📋 Mathlib.CategoryTheory.Category.Cat
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] : ↑(CategoryTheory.Cat.of C) = C
• CategoryTheory.typeToCat_obj 📋 Mathlib.CategoryTheory.Category.Cat
  (X : Type u) : CategoryTheory.typeToCat.obj X = CategoryTheory.Cat.of (CategoryTheory.Discrete X)
• CategoryTheory.Functor.toCatHom 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Cat.of C ⟶ CategoryTheory.Cat.of D
• CategoryTheory.Functor.equivCatHom 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] : CategoryTheory.Functor C D ≃ (CategoryTheory.Cat.of C ⟶ CategoryTheory.Cat.of D)
• CategoryTheory.Functor.toCatHom_toFunctor 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) : F.toCatHom.toFunctor = F
• CategoryTheory.Cat.Hom.isoMk 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) : F.toCatHom ≅ G.toCatHom
• CategoryTheory.NatTrans.toCatHom₂ 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) : F.toCatHom ⟶ G.toCatHom
• CategoryTheory.NatTrans.toCatHom₂_toNatTrans 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (η : F ⟶ G) : (CategoryTheory.NatTrans.toCatHom₂ η).toNatTrans = η
• CategoryTheory.NatTrans.toCatHom₂_id 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) : CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.toCatHom
• CategoryTheory.Cat.Hom.isoMk_toNatIso 📋 Mathlib.CategoryTheory.Category.Cat
  {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) : CategoryTheory.Cat.Hom.isoMk (CategoryTheory.Cat.Hom.toNatIso e) = e
• CategoryTheory.typeToCat_map 📋 Mathlib.CategoryTheory.Category.Cat
  {X✝ Y✝ : Type u} (f : X✝ ⟶ Y✝) : CategoryTheory.typeToCat.map f = (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑(CategoryTheory.ConcreteCategory.hom f))).toCatHom
• CategoryTheory.Functor.equivCatHom_apply 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (F : CategoryTheory.Functor C D) : (CategoryTheory.Functor.equivCatHom C D) F = F.toCatHom
• CategoryTheory.Cat.Hom.isoMk_hom 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) : (CategoryTheory.Cat.Hom.isoMk e).hom = CategoryTheory.NatTrans.toCatHom₂ e.hom
• CategoryTheory.Cat.Hom.isoMk_inv 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) : (CategoryTheory.Cat.Hom.isoMk e).inv = CategoryTheory.NatTrans.toCatHom₂ e.inv
• CategoryTheory.Cat.Hom.toNatIso_isoMk 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) : CategoryTheory.Cat.Hom.toNatIso (CategoryTheory.Cat.Hom.isoMk e) = e
• CategoryTheory.Cat.Hom.equivFunctor_apply 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : CategoryTheory.Cat) (a✝ : CategoryTheory.Cat.of ↑C ⟶ CategoryTheory.Cat.of ↑D) : (CategoryTheory.Cat.Hom.equivFunctor C D) a✝ = a✝.toFunctor
• CategoryTheory.Functor.equivCatHom_symm_apply 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] (self : (CategoryTheory.Cat.of C).Hom (CategoryTheory.Cat.of D)) : (CategoryTheory.Functor.equivCatHom C D).symm self = self.toFunctor
• CategoryTheory.Cat.Hom.equivFunctor_symm_apply 📋 Mathlib.CategoryTheory.Category.Cat
  (C D : CategoryTheory.Cat) (a✝ : CategoryTheory.Functor ↑C ↑D) : (CategoryTheory.Cat.Hom.equivFunctor C D).symm a✝ = a✝.toCatHom
• CategoryTheory.NatTrans.toCatHom₂_comp 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F G H : CategoryTheory.Functor C D} (η₁ : F ⟶ G) (η₂ : G ⟶ H) : CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.CategoryStruct.comp η₁ η₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.toCatHom₂ η₁) (CategoryTheory.NatTrans.toCatHom₂ η₂)
• CategoryTheory.Cat.isoOfEquiv_hom 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯ := by cat_disch) : (CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄).hom = e.functor.toCatHom
• CategoryTheory.Cat.isoOfEquiv_inv 📋 Mathlib.CategoryTheory.Category.Cat
  {C D : CategoryTheory.Cat} (e : ↑C ≌ ↑D) (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) (h₃ : ∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯ := by cat_disch) (h₄ : ∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯ := by cat_disch) : (CategoryTheory.Cat.isoOfEquiv e h₁ h₂ h₃ h₄).inv = e.inverse.toCatHom
• CategoryTheory.Over.mapFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] (X : T) : (CategoryTheory.Over.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Over X)
• CategoryTheory.Under.mapFunctor_obj 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] (X : Tᵒᵖ) : (CategoryTheory.Under.mapFunctor T).obj X = CategoryTheory.Cat.of (CategoryTheory.Under (Opposite.unop X))
• CategoryTheory.Over.mapFunctor_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] {X✝ Y✝ : T} (f : X✝ ⟶ Y✝) : (CategoryTheory.Over.mapFunctor T).map f = (CategoryTheory.Over.map f).toCatHom
• CategoryTheory.Under.mapFunctor_map 📋 Mathlib.CategoryTheory.Comma.Over.Basic
  (T : Type u₁) [CategoryTheory.Category.{v₁, u₁} T] {X✝ Y✝ : Tᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Under.mapFunctor T).map f = (CategoryTheory.Under.map f.unop).toCatHom
• preordToCat_obj 📋 Mathlib.Order.Category.Preord
  (X : Preord) : preordToCat.obj X = CategoryTheory.Cat.of ↑X
• preordToCat_map 📋 Mathlib.Order.Category.Preord
  {X✝ Y✝ : Preord} (f : X✝ ⟶ Y✝) : preordToCat.map f = ⋯.functor.toCatHom
• CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : CategoryTheory.Cat) : CategoryTheory.WithInitial.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithInitial ↑C)
• CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_obj 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : CategoryTheory.Cat) : CategoryTheory.WithTerminal.prelaxfunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.WithTerminal ↑C)
• CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) : CategoryTheory.WithInitial.prelaxfunctor.map F = (CategoryTheory.WithInitial.map F.toFunctor).toCatHom
• CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_toPrefunctor_map 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) : CategoryTheory.WithTerminal.prelaxfunctor.map F = (CategoryTheory.WithTerminal.map F.toFunctor).toCatHom
• CategoryTheory.WithInitial.prelaxfunctor_toPrelaxFunctorStruct_map₂ 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ : CategoryTheory.Cat} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) : CategoryTheory.WithInitial.prelaxfunctor.map₂ f = CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.WithInitial.map₂ f.toNatTrans)
• CategoryTheory.WithTerminal.prelaxfunctor_toPrelaxFunctorStruct_map₂ 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ : CategoryTheory.Cat} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) : CategoryTheory.WithTerminal.prelaxfunctor.map₂ f = CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.WithTerminal.map₂ f.toNatTrans)
• CategoryTheory.WithInitial.pseudofunctor_mapId 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : CategoryTheory.Cat) : CategoryTheory.WithInitial.pseudofunctor.mapId C = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithInitial.mapId ↑C)
• CategoryTheory.WithTerminal.pseudofunctor_mapId 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  (C : CategoryTheory.Cat) : CategoryTheory.WithTerminal.pseudofunctor.mapId C = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithTerminal.mapId ↑C)
• CategoryTheory.WithInitial.pseudofunctor_mapComp 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ c✝ : CategoryTheory.Cat} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CategoryTheory.WithInitial.pseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithInitial.mapComp x✝.toFunctor x✝¹.toFunctor)
• CategoryTheory.WithTerminal.pseudofunctor_mapComp 📋 Mathlib.CategoryTheory.WithTerminal.Basic
  {a✝ b✝ c✝ : CategoryTheory.Cat} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CategoryTheory.WithTerminal.pseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithTerminal.mapComp x✝.toFunctor x✝¹.toFunctor)
• CategoryTheory.Cat.asSmallFunctor_obj 📋 Mathlib.CategoryTheory.Category.Cat.AsSmall
  (C : CategoryTheory.Cat) : CategoryTheory.Cat.asSmallFunctor.obj C = CategoryTheory.Cat.of (CategoryTheory.AsSmall ↑C)
• CategoryTheory.Cat.asSmallFunctor_map 📋 Mathlib.CategoryTheory.Category.Cat.AsSmall
  {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) : CategoryTheory.Cat.asSmallFunctor.map F = (CategoryTheory.AsSmall.down.comp (F.toFunctor.comp CategoryTheory.AsSmall.up)).toCatHom
• CategoryTheory.Functor.elementsFunctor_obj 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) : CategoryTheory.Functor.elementsFunctor.obj F = CategoryTheory.Cat.of F.Elements
• CategoryTheory.Functor.elementsFunctor_map 📋 Mathlib.CategoryTheory.Elements
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Functor C (Type w)} (n : X✝ ⟶ Y✝) : CategoryTheory.Functor.elementsFunctor.map n = (CategoryTheory.NatTrans.mapElements n).toCatHom
• CategoryTheory.Grothendieck.mapIdIso 📋 Mathlib.CategoryTheory.Grothendieck
  {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} : (CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.id F)).toCatHom ≅ CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (CategoryTheory.Grothendieck F))
• CategoryTheory.CostructuredArrow.functor_obj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) (d : D) : (CategoryTheory.CostructuredArrow.functor T).obj d = CategoryTheory.Cat.of (CategoryTheory.CostructuredArrow T d)
• CategoryTheory.StructuredArrow.functor_obj 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) (d : Dᵒᵖ) : (CategoryTheory.StructuredArrow.functor T).obj d = CategoryTheory.Cat.of (CategoryTheory.StructuredArrow (Opposite.unop d) T)
• CategoryTheory.CostructuredArrow.functor_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : (CategoryTheory.CostructuredArrow.functor T).map f = (CategoryTheory.CostructuredArrow.map f).toCatHom
• CategoryTheory.StructuredArrow.functor_map 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (T : CategoryTheory.Functor C D) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.StructuredArrow.functor T).map f = (CategoryTheory.StructuredArrow.map f.unop).toCatHom
• CategoryTheory.CostructuredArrow.preFunctor_app 📋 Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (S : CategoryTheory.Functor C D) (T : CategoryTheory.Functor D E) (e : E) : (CategoryTheory.CostructuredArrow.preFunctor S T).app e = (CategoryTheory.CostructuredArrow.pre S T e).toCatHom
• CategoryTheory.Cat.free_obj 📋 Mathlib.CategoryTheory.Category.Quiv
  (V : CategoryTheory.Quiv) : CategoryTheory.Cat.free.obj V = CategoryTheory.Cat.of (CategoryTheory.Paths ↑V)
• CategoryTheory.Cat.free_map 📋 Mathlib.CategoryTheory.Category.Quiv
  {X✝ Y✝ : CategoryTheory.Quiv} (F : X✝ ⟶ Y✝) : CategoryTheory.Cat.free.map F = (CategoryTheory.Cat.freeMap (CategoryTheory.Prefunctor.ofQuivHom F)).toCatHom
• CategoryTheory.Quiv.adj_homEquiv 📋 Mathlib.CategoryTheory.Category.Quiv
  {V C : Type u} [Quiver V] [CategoryTheory.Category.{max u v, u} C] : CategoryTheory.Quiv.adj.homEquiv (CategoryTheory.Quiv.of V) (CategoryTheory.Cat.of C) = (CategoryTheory.Cat.Hom.equivFunctor (CategoryTheory.Cat.of (CategoryTheory.Paths V)) (CategoryTheory.Cat.of C)).trans CategoryTheory.Quiv.pathsEquiv
• CommRingCat.moduleCatExtendScalarsPseudofunctor_obj 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  (b : CategoryTheory.LocallyDiscrete CommRingCat) : CommRingCat.moduleCatExtendScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑b.as)
• RingCat.moduleCatRestrictScalarsPseudofunctor_obj 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  (b : CategoryTheory.LocallyDiscrete RingCatᵒᵖ) : RingCat.moduleCatRestrictScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑(Opposite.unop b.as))
• CommRingCat.moduleCatRestrictScalarsPseudofunctor_obj 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  (b : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.obj b = CategoryTheory.Cat.of (ModuleCat ↑(Opposite.unop b.as))
• CommRingCat.moduleCatExtendScalarsPseudofunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete CommRingCat} (f : X✝ ⟶ Y✝) : CommRingCat.moduleCatExtendScalarsPseudofunctor.map f = (ModuleCat.extendScalars (CommRingCat.Hom.hom f.as)).toCatHom
• RingCat.moduleCatRestrictScalarsPseudofunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete RingCatᵒᵖ} (f : X✝ ⟶ Y✝) : RingCat.moduleCatRestrictScalarsPseudofunctor.map f = (ModuleCat.restrictScalars (RingCat.Hom.hom f.as.unop)).toCatHom
• CommRingCat.moduleCatRestrictScalarsPseudofunctor_map 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ} (f : X✝ ⟶ Y✝) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.map f = (ModuleCat.restrictScalars (CommRingCat.Hom.hom f.as.unop)).toCatHom
• CommRingCat.moduleCatExtendScalarsPseudofunctor_mapId 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  (x✝ : CategoryTheory.LocallyDiscrete CommRingCat) : CommRingCat.moduleCatExtendScalarsPseudofunctor.mapId x✝ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.extendScalarsId ↑x✝.as)
• RingCat.moduleCatRestrictScalarsPseudofunctor_mapId 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  (x✝ : CategoryTheory.LocallyDiscrete RingCatᵒᵖ) : RingCat.moduleCatRestrictScalarsPseudofunctor.mapId x✝ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsId ↑(Opposite.unop x✝.as))
• CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapId 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  (x✝ : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.mapId x✝ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsId ↑(Opposite.unop x✝.as))
• CommRingCat.moduleCatExtendScalarsPseudofunctor_mapComp 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete CommRingCat} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CommRingCat.moduleCatExtendScalarsPseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.extendScalarsComp (CommRingCat.Hom.hom x✝.as) (CommRingCat.Hom.hom x✝¹.as))
• RingCat.moduleCatRestrictScalarsPseudofunctor_mapComp 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete RingCatᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : RingCat.moduleCatRestrictScalarsPseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsComp (RingCat.Hom.hom x✝¹.as.unop) (RingCat.Hom.hom x✝.as.unop))
• CommRingCat.moduleCatRestrictScalarsPseudofunctor_mapComp 📋 Mathlib.Algebra.Category.ModuleCat.Pseudofunctor
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete CommRingCatᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : CommRingCat.moduleCatRestrictScalarsPseudofunctor.mapComp x✝ x✝¹ = CategoryTheory.Cat.Hom.isoMk (ModuleCat.restrictScalarsComp (CommRingCat.Hom.hom x✝¹.as.unop) (CommRingCat.Hom.hom x✝.as.unop))
• SimplexCategory.toCat_obj 📋 Mathlib.AlgebraicTopology.SimplexCategory.Basic
  (X : SimplexCategory) : SimplexCategory.toCat.obj X = CategoryTheory.Cat.of ↑((CategoryTheory.forget₂ PartOrd Preord).obj ((CategoryTheory.forget₂ Lat PartOrd).obj ((CategoryTheory.forget₂ LinOrd Lat).obj ((CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd).obj (NonemptyFinLinOrd.of (Fin (X.len + 1)))))))
• CategoryTheory.Adjunction.toCat 📋 Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : CategoryTheory.Bicategory.Adjunction F.toCatHom G.toCatHom
• CategoryTheory.Adjunction.toCat_ofCat 📋 Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
  {C D : CategoryTheory.Cat} {F : C ⟶ D} {G : D ⟶ C} (adj : CategoryTheory.Bicategory.Adjunction F G) : (CategoryTheory.Adjunction.ofCat adj).toCat = adj
• CategoryTheory.Adjunction.ofCat_toCat 📋 Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : CategoryTheory.Adjunction.ofCat adj.toCat = adj
• CategoryTheory.Adjunction.toCat_counit_toNatTrans 📋 Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : adj.toCat.counit.toNatTrans = adj.counit
• CategoryTheory.Adjunction.toCat_unit_toNatTrans 📋 Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
  {C D : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : adj.toCat.unit.toNatTrans = adj.unit
• CategoryTheory.Adjunction.toCat_comp_toCat 📋 Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
  {C D E : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Category.{v, u} D] [CategoryTheory.Category.{v, u} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {F' : CategoryTheory.Functor D E} {G' : CategoryTheory.Functor E D} (adj' : F' ⊣ G') : adj.toCat.comp adj'.toCat = (adj.comp adj').toCat
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_obj_obj 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  (b : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.obj b).obj = CategoryTheory.Cat.of (Opposite.unop b.as).Modules
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_l 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).l = (AlgebraicGeometry.Scheme.Modules.pullback f.as.unop).toCatHom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_r 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).r = (AlgebraicGeometry.Scheme.Modules.pushforward f.as.unop).toCatHom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_map_adj 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {X✝ Y✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (f : X✝ ⟶ Y✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.map f).adj = (AlgebraicGeometry.Scheme.Modules.pullbackPushforwardAdjunction f.as.unop).toCat
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  (x✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x✝).hom.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackId (Opposite.unop x✝.as)).hom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  (x✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x✝).inv.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackId (Opposite.unop x✝.as)).inv
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_hom_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  (x✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x✝).hom.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardId (Opposite.unop x✝.as)).inv
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapId_inv_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  (x✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapId x✝).inv.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardId (Opposite.unop x✝.as)).hom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).hom.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackComp x✝¹.as.unop x✝.as.unop).inv
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τl 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).inv.τl = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pullbackComp x✝¹.as.unop x✝.as.unop).hom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_hom_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).hom.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardComp x✝¹.as.unop x✝.as.unop).hom
• AlgebraicGeometry.Scheme.Modules.pseudofunctor_mapComp_inv_τr 📋 Mathlib.AlgebraicGeometry.Modules.Sheaf
  {a✝ b✝ c✝ : CategoryTheory.LocallyDiscrete AlgebraicGeometry.Schemeᵒᵖ} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (AlgebraicGeometry.Scheme.Modules.pseudofunctor.mapComp x✝ x✝¹).inv.τr = CategoryTheory.NatTrans.toCatHom₂ (AlgebraicGeometry.Scheme.Modules.pushforwardComp x✝¹.as.unop x✝.as.unop).inv
• CategoryTheory.Monoidal.tensorObj 📋 Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
  (C D : CategoryTheory.Cat) : CategoryTheory.MonoidalCategoryStruct.tensorObj C D = CategoryTheory.Cat.of (↑C × ↑D)
• CategoryTheory.Cat.freeRefl_obj 📋 Mathlib.CategoryTheory.Category.ReflQuiv
  (V : CategoryTheory.ReflQuiv) : CategoryTheory.Cat.freeRefl.obj V = CategoryTheory.Cat.of (CategoryTheory.Cat.FreeRefl ↑V)
• CategoryTheory.Cat.freeRefl_map 📋 Mathlib.CategoryTheory.Category.ReflQuiv
  {X✝ Y✝ : CategoryTheory.ReflQuiv} (F : X✝ ⟶ Y✝) : CategoryTheory.Cat.freeRefl.map F = (CategoryTheory.Cat.freeReflMap F).toCatHom
• CategoryTheory.ReflQuiv.adj_counit_app 📋 Mathlib.CategoryTheory.Category.ReflQuiv
  (D : Type u) [CategoryTheory.Category.{max u v, u} D] : CategoryTheory.ReflQuiv.adj.counit.app (CategoryTheory.Cat.of D) = (CategoryTheory.Cat.FreeRefl.lift (𝟭rq D)).toCatHom
• CategoryTheory.ReflQuiv.forget_faithful 📋 Mathlib.CategoryTheory.Category.ReflQuiv
  {C D : CategoryTheory.Cat} (F G : CategoryTheory.Functor ↑C ↑D) (hyp : CategoryTheory.ReflQuiv.forget.map F.toCatHom = CategoryTheory.ReflQuiv.forget.map G.toCatHom) : F = G
• CategoryTheory.ReflQuiv.adj_homEquiv 📋 Mathlib.CategoryTheory.Category.ReflQuiv
  (V : Type u) [CategoryTheory.ReflQuiver V] (C : Type u) [CategoryTheory.Category.{max u v, u} C] : CategoryTheory.ReflQuiv.adj.homEquiv (CategoryTheory.ReflQuiv.of V) (CategoryTheory.Cat.of C) = (CategoryTheory.Cat.Hom.equivFunctor (CategoryTheory.Cat.freeRefl.obj (CategoryTheory.ReflQuiv.of V)) (CategoryTheory.Cat.of C)).trans CategoryTheory.ReflQuiv.adj.homEquiv
• CategoryTheory.ReflQuiv.adj.counit.comp_app_eq 📋 Mathlib.CategoryTheory.Category.ReflQuiv
  (C : Type u) [CategoryTheory.Category.{max u v, u} C] : (CategoryTheory.Cat.FreeRefl.quotientFunctor C).comp (CategoryTheory.ReflQuiv.adj.counit.app (CategoryTheory.Cat.of C)).toFunctor = CategoryTheory.pathComposition C
• CategoryTheory.Cat.isTerminalDiscretePUnit 📋 Mathlib.CategoryTheory.Category.Cat.Terminal
  : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of (CategoryTheory.Discrete PUnit.{u_1 + 1}))
• CategoryTheory.Cat.isTerminalOfUniqueOfIsDiscrete 📋 Mathlib.CategoryTheory.Category.Cat.Terminal
  {T : Type u} [CategoryTheory.Category.{v, u} T] [Unique T] [CategoryTheory.IsDiscrete T] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of T)
• CategoryTheory.Cat.terminalIsoOfUniqueOfIsDiscrete 📋 Mathlib.CategoryTheory.Category.Cat.Terminal
  {T : Type u} [CategoryTheory.Category.{v, u} T] [Unique T] [CategoryTheory.IsDiscrete T] : ⊤_ CategoryTheory.Cat ≅ CategoryTheory.Cat.of T
• CategoryTheory.Cat.isoDiscretePUnitOfIsTerminal 📋 Mathlib.CategoryTheory.Category.Cat.Terminal
  {T : Type u} [CategoryTheory.Category.{u, u} T] (hT : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of T)) : CategoryTheory.Cat.of T ≅ CategoryTheory.Cat.of (CategoryTheory.Discrete PUnit.{u + 1})
• SSet.hoFunctor_obj 📋 Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
  (X : SSet) : SSet.hoFunctor.obj X = CategoryTheory.Cat.of X.HomotopyCategory
• SSet.Truncated.HomotopyCategory.isTerminal 📋 Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
  (X : SSet.Truncated 2) [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }))] [Subsingleton (X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.ι0₂._proof_5 }))] : CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of X.HomotopyCategory)
• SSet.hoFunctor_map 📋 Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
  {X✝ Y✝ : SSet} (f : X✝ ⟶ Y✝) : SSet.hoFunctor.map f = (SSet.mapHomotopyCategory f).toCatHom
• SSet.Truncated.HomotopyCategory.isoTerminal 📋 Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
  (X : SSet.Truncated 2) [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))] [Subsingleton (X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.HomotopyCategory.isoTerminal._proof_1 }))] : CategoryTheory.Cat.of X.HomotopyCategory ≅ CategoryTheory.Cat.chosenTerminal
• SSet.Truncated.HomotopyCategory.BinaryProduct.iso 📋 Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
  (X Y : SSet.Truncated 2) : CategoryTheory.Cat.of (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory ≅ CategoryTheory.Cat.of (X.HomotopyCategory × Y.HomotopyCategory)
• SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor 📋 Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
  (X Y : SSet.Truncated 2) : (SSet.Truncated.HomotopyCategory.BinaryProduct.iso X Y).hom.toFunctor = SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y
• SSet.Truncated.HomotopyCategory.BinaryProduct.iso_inv_toFunctor 📋 Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
  (X Y : SSet.Truncated 2) : (SSet.Truncated.HomotopyCategory.BinaryProduct.iso X Y).inv.toFunctor = SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y
• SSet.Truncated.HomotopyCategory.BinaryProduct.left_unitality 📋 Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
  (X Y : SSet.Truncated 2) [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))] [Subsingleton (X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.HomotopyCategory.isoTerminal._proof_1 }))] : CategoryTheory.Prod.snd (↑CategoryTheory.Cat.chosenTerminal) Y.HomotopyCategory = ((SSet.Truncated.HomotopyCategory.isoTerminal X).inv.toFunctor.prod (CategoryTheory.Functor.id Y.HomotopyCategory)).comp ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp (SSet.Truncated.mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)))
• SSet.Truncated.HomotopyCategory.BinaryProduct.right_unitality 📋 Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
  (X Y : SSet.Truncated 2) [Unique (Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))] [Subsingleton (Y.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.HomotopyCategory.isoTerminal._proof_1 }))] : CategoryTheory.Prod.fst X.HomotopyCategory ↑CategoryTheory.Cat.chosenTerminal = ((CategoryTheory.Functor.id X.HomotopyCategory).prod (SSet.Truncated.HomotopyCategory.isoTerminal Y).inv.toFunctor).comp ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp (SSet.Truncated.mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)))
• CategoryTheory.Cat.closed 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  (C : Type u) [CategoryTheory.Category.{u, u} C] : CategoryTheory.Closed (CategoryTheory.Cat.of C)
• CategoryTheory.Cat.exp_obj 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  (C : Type u) [CategoryTheory.Category.{v, u} C] (D : CategoryTheory.Cat) : (CategoryTheory.Cat.exp C).obj D = CategoryTheory.Cat.of (CategoryTheory.Functor C ↑D)
• CategoryTheory.Cat.ihom_obj 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  (C : Type u) [CategoryTheory.Category.{u, u} C] (D : Type u) [CategoryTheory.Category.{u, u} D] : (CategoryTheory.Cat.of C ⟹ CategoryTheory.Cat.of D) = CategoryTheory.Cat.of (CategoryTheory.Functor C D)
• CategoryTheory.curryingIso 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : CategoryTheory.Cat.of (CategoryTheory.Functor C (CategoryTheory.Functor D E)) ≅ CategoryTheory.Cat.of (CategoryTheory.Functor (C × D) E)
• CategoryTheory.flippingIso 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] : CategoryTheory.Cat.of (CategoryTheory.Functor C (CategoryTheory.Functor D E)) ≅ CategoryTheory.Cat.of (CategoryTheory.Functor D (CategoryTheory.Functor C E))
• CategoryTheory.Cat.ihom_map 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  (C : Type u) [CategoryTheory.Category.{u, u} C] {D E : Type u} [CategoryTheory.Category.{u, u} D] [CategoryTheory.Category.{u, u} E] (F : CategoryTheory.Functor D E) : (CategoryTheory.ihom (CategoryTheory.Cat.of C)).map F.toCatHom = ((CategoryTheory.Functor.whiskeringRight C D E).obj F).toCatHom
• CategoryTheory.Cat.exp_map 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) : (CategoryTheory.Cat.exp C).map F = ((CategoryTheory.Functor.whiskeringRight C ↑X✝ ↑Y✝).obj F.toFunctor).toCatHom
• CategoryTheory.curryingIso_inv_toFunctor_obj_obj_obj 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) (Y : D) : ((CategoryTheory.curryingIso.inv.toFunctor.obj F).obj X).obj Y = F.obj (X, Y)
• CategoryTheory.curryingIso_hom_toFunctor_obj_obj 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : C × D) : (CategoryTheory.curryingIso.hom.toFunctor.obj F).obj X = (F.obj X.1).obj X.2
• CategoryTheory.flippingIso_hom_toFunctor_obj_obj_obj 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) (j : C) : ((CategoryTheory.flippingIso.hom.toFunctor.obj F).obj k).obj j = (F.obj j).obj k
• CategoryTheory.flippingIso_inv_toFunctor_obj_obj_obj 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (k : C) (j : D) : ((CategoryTheory.flippingIso.inv.toFunctor.obj F).obj k).obj j = (F.obj j).obj k
• CategoryTheory.curryingIso_inv_toFunctor_obj_obj_map 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) (X : C) {X✝ Y✝ : D} (g : X✝ ⟶ Y✝) : ((CategoryTheory.curryingIso.inv.toFunctor.obj F).obj X).map g = F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)
• CategoryTheory.flippingIso_hom_toFunctor_obj_obj_map 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (k : D) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.flippingIso.hom.toFunctor.obj F).obj k).map f = (F.map f).app k
• CategoryTheory.flippingIso_inv_toFunctor_obj_obj_map 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (k : C) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) : ((CategoryTheory.flippingIso.inv.toFunctor.obj F).obj k).map f = (F.map f).app k
• CategoryTheory.curryingIso_inv_toFunctor_map_app_app 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] {X✝ Y✝ : CategoryTheory.Functor (C × D) E} (T : X✝ ⟶ Y✝) (X : C) (Y : D) : ((CategoryTheory.curryingIso.inv.toFunctor.map T).app X).app Y = T.app (X, Y)
• CategoryTheory.flippingIso_hom_toFunctor_map_app_app 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] {F₁ F₂ : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (φ : F₁ ⟶ F₂) (Y : D) (X : C) : ((CategoryTheory.flippingIso.hom.toFunctor.map φ).app Y).app X = (φ.app X).app Y
• CategoryTheory.flippingIso_inv_toFunctor_map_app_app 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] {F₁ F₂ : CategoryTheory.Functor D (CategoryTheory.Functor C E)} (φ : F₁ ⟶ F₂) (Y : C) (X : D) : ((CategoryTheory.flippingIso.inv.toFunctor.map φ).app Y).app X = (φ.app X).app Y
• CategoryTheory.flippingIso_hom_toFunctor_obj_map_app 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) (j : C) : ((CategoryTheory.flippingIso.hom.toFunctor.obj F).map f).app j = (F.obj j).map f
• CategoryTheory.flippingIso_inv_toFunctor_obj_map_app 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (j : D) : ((CategoryTheory.flippingIso.inv.toFunctor.obj F).map f).app j = (F.obj j).map f
• CategoryTheory.curryingIso_hom_toFunctor_obj_map 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) {X Y : C × D} (f : X ⟶ Y) : (CategoryTheory.curryingIso.hom.toFunctor.obj F).map f = CategoryTheory.CategoryStruct.comp ((F.map f.1).app X.2) ((F.obj Y.1).map f.2)
• CategoryTheory.curryingIso_inv_toFunctor_obj_map_app 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × D) E) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (Y : D) : ((CategoryTheory.curryingIso.inv.toFunctor.obj F).map f).app Y = F.map (CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id Y))
• CategoryTheory.curryingIso_hom_toFunctor_map_app 📋 Mathlib.CategoryTheory.Category.Cat.CartesianClosed
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄} [CategoryTheory.Category.{v₄, u₄} E] {X✝ Y✝ : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X✝ ⟶ Y✝) (X : C × D) : (CategoryTheory.curryingIso.hom.toFunctor.map T).app X = (T.app X.1).app X.2
• CategoryTheory.nerve.functorOfNerveMap_nerveFunctor₂_map 📋 Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
  {C D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (F : CategoryTheory.Functor C D) : CategoryTheory.nerve.functorOfNerveMap ((SSet.truncation 2).map (CategoryTheory.nerveMap F)) = F
• CategoryTheory.nerve.functorOfNerveMap 📋 Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
  {C D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (φ : CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of C) ⟶ CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of D)) : CategoryTheory.Functor C D
• CategoryTheory.nerve.nerveFunctor₂_map_functorOfNerveMap 📋 Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
  {C D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (φ : CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of C) ⟶ CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of D)) : CategoryTheory.Nerve.nerveFunctor₂.map (CategoryTheory.nerve.functorOfNerveMap φ).toCatHom = φ
• CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf 📋 Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
  (C D : Type u) [CategoryTheory.Category.{u, u} C] [CategoryTheory.Category.{u, u} D] : CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison (CategoryTheory.nerveFunctor.comp (SSet.hoFunctor.comp CategoryTheory.nerveFunctor)) (CategoryTheory.Cat.of C) (CategoryTheory.Cat.of D))
• CategoryTheory.nerve.functorOfNerveMap_obj 📋 Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
  {C D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (φ : CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of C) ⟶ CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of D)) (x : C) : (CategoryTheory.nerve.functorOfNerveMap φ).obj x = CategoryTheory.nerveEquiv ((CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op { obj := { len := 0 }, property := _proof_12✝ }))) (CategoryTheory.nerveEquiv.symm x))
• CategoryTheory.nerve.functorOfNerveMap_map 📋 Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
  {C D : Type u} [CategoryTheory.SmallCategory C] [CategoryTheory.SmallCategory D] (φ : CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of C) ⟶ CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of D)) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.nerve.functorOfNerveMap φ).map f = CategoryTheory.nerve.homEquiv ((CategoryTheory.nerve.edgeMk f).toTruncated.map φ)
• CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj 📋 Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
  {B : Type u} [CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] (X : B) : P.fullsubcategory.obj X = CategoryTheory.Cat.of (P.Obj X)
• CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor 📋 Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
  {B : Type u} [CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {X✝ Y✝ : B} (f : X✝ ⟶ Y✝) : (P.fullsubcategory.map f).toFunctor = P.map f
• CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapId 📋 Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
  {B : Type u} [CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] (X : B) : P.fullsubcategory.mapId X = CategoryTheory.Cat.Hom.isoMk (P.mapId X)
• CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans 📋 Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
  {B : Type u} [CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {a✝ b✝ : B} {f✝ g✝ : a✝ ⟶ b✝} (α : f✝ ⟶ g✝) : (P.fullsubcategory.map₂ α).toNatTrans = P.map₂ α
• CategoryTheory.Pseudofunctor.ObjectProperty.fullsubcategory_mapComp 📋 Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
  {B : Type u} [CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} (P : F.ObjectProperty) [P.IsClosedUnderMapObj] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : P.fullsubcategory.mapComp f g = CategoryTheory.Cat.Hom.isoMk (P.mapComp f g)
• CategoryTheory.Bicategory.postcomposingCat 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b c : B) : CategoryTheory.Functor (b ⟶ c) (CategoryTheory.Cat.of (a ⟶ b) ⟶ CategoryTheory.Cat.of (a ⟶ c))
• CategoryTheory.Bicategory.precomposingCat 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b c : B) : CategoryTheory.Functor (a ⟶ b) (CategoryTheory.Cat.of (b ⟶ c) ⟶ CategoryTheory.Cat.of (a ⟶ c))
• CategoryTheory.Bicategory.postcomp₂_app_toFunctor_obj 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : ((CategoryTheory.Bicategory.postcomp₂ f).app x).toFunctor.obj x✝ = CategoryTheory.CategoryStruct.comp x✝ f
• CategoryTheory.Bicategory.postcomposingCat_obj 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b c : B) (f : b ⟶ c) : (CategoryTheory.Bicategory.postcomposingCat a b c).obj f = (CategoryTheory.Bicategory.postcomp a f).toCatHom
• CategoryTheory.Bicategory.precomposingCat_obj 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b c : B) (f : a ⟶ b) : (CategoryTheory.Bicategory.precomposingCat a b c).obj f = (CategoryTheory.Bicategory.precomp c f).toCatHom
• CategoryTheory.Bicategory.leftUnitorNatIsoCat 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) : (CategoryTheory.Bicategory.precomposingCat a a b).obj (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (a ⟶ b))
• CategoryTheory.Bicategory.rightUnitorNatIsoCat 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) : (CategoryTheory.Bicategory.postcomposingCat a b b).obj (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (a ⟶ b))
• CategoryTheory.Bicategory.postcomposing₂_obj_app_toFunctor_obj 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : (((CategoryTheory.Bicategory.postcomposing₂ a b).obj f).app x).toFunctor.obj x✝ = CategoryTheory.CategoryStruct.comp x✝ f
• CategoryTheory.Bicategory.postcomp₂_app_toFunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) (x : Bᵒᵖ) {X✝ Y✝ : Opposite.unop x ⟶ a} (x✝ : X✝ ⟶ Y✝) : ((CategoryTheory.Bicategory.postcomp₂ f).app x).toFunctor.map x✝ = CategoryTheory.Bicategory.whiskerRight x✝ f
• CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x : B) {a b : Bᵒᵖ} (a✝ : a ⟶ b) (x✝ : Opposite.unop a ⟶ x) : ((CategoryTheory.Bicategory.yoneda₀ x).map a✝).toFunctor.obj x✝ = CategoryTheory.CategoryStruct.comp a✝.unop x✝
• CategoryTheory.Bicategory.postcomposing₂_obj_app_toFunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b) (x : Bᵒᵖ) {X✝ Y✝ : Opposite.unop x ⟶ a} (x✝ : X✝ ⟶ Y✝) : (((CategoryTheory.Bicategory.postcomposing₂ a b).obj f).app x).toFunctor.map x✝ = CategoryTheory.Bicategory.whiskerRight x✝ f
• CategoryTheory.Bicategory.associatorNatIsoRightCat 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) : (CategoryTheory.Bicategory.precomposingCat a c d).obj (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.precomposingCat b c d).obj g) ((CategoryTheory.Bicategory.precomposingCat a b d).obj f)
• CategoryTheory.Bicategory.associatorNatIsoLeftCat 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a : B) {b c d : B} (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.postcomposingCat a b c).obj g) ((CategoryTheory.Bicategory.postcomposingCat a c d).obj h) ≅ (CategoryTheory.Bicategory.postcomposingCat a b d).obj (CategoryTheory.CategoryStruct.comp g h)
• CategoryTheory.Bicategory.postcomposingCat_map 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b c : B) {X✝ Y✝ : b ⟶ c} (η : X✝ ⟶ Y✝) : (CategoryTheory.Bicategory.postcomposingCat a b c).map η = CategoryTheory.NatTrans.toCatHom₂ ((CategoryTheory.Bicategory.postcomposing a b c).map η)
• CategoryTheory.Bicategory.precomposingCat_map 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b c : B) {X✝ Y✝ : a ⟶ b} (η : X✝ ⟶ Y✝) : (CategoryTheory.Bicategory.precomposingCat a b c).map η = CategoryTheory.NatTrans.toCatHom₂ ((CategoryTheory.Bicategory.precomposing a b c).map η)
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_obj 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (a✝ : a ⟶ b) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : ((CategoryTheory.Bicategory.yoneda.map a✝).app x).toFunctor.obj x✝ = CategoryTheory.CategoryStruct.comp x✝ a✝
• CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x : B) {a b : Bᵒᵖ} (a✝ : a ⟶ b) {X✝ Y✝ : Opposite.unop a ⟶ x} (x✝ : X✝ ⟶ Y✝) : ((CategoryTheory.Bicategory.yoneda₀ x).map a✝).toFunctor.map x✝ = CategoryTheory.Bicategory.whiskerLeft a✝.unop x✝
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_app_toFunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (a✝ : a ⟶ b) (x : Bᵒᵖ) {X✝ Y✝ : Opposite.unop x ⟶ a} (x✝ : X✝ ⟶ Y✝) : ((CategoryTheory.Bicategory.yoneda.map a✝).app x).toFunctor.map x✝ = CategoryTheory.Bicategory.whiskerRight x✝ a✝
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x✝ : B) {a b : Bᵒᵖ} (a✝ : a ⟶ b) (x✝¹ : Opposite.unop a ⟶ x✝) : ((CategoryTheory.Bicategory.yoneda.obj x✝).map a✝).toFunctor.obj x✝¹ = CategoryTheory.CategoryStruct.comp a✝.unop x✝¹
• CategoryTheory.Bicategory.associatorNatIsoMiddleCat 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.precomposingCat a b c).obj f) ((CategoryTheory.Bicategory.postcomposingCat a c d).obj h) ≅ CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.postcomposingCat b c d).obj h) ((CategoryTheory.Bicategory.precomposingCat a b d).obj f)
• CategoryTheory.Bicategory.leftUnitorNatIsoCat_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b) : (CategoryTheory.Bicategory.leftUnitorNatIsoCat a b).hom.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).hom
• CategoryTheory.Bicategory.leftUnitorNatIsoCat_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b) : (CategoryTheory.Bicategory.leftUnitorNatIsoCat a b).inv.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).inv
• CategoryTheory.Bicategory.rightUnitorNatIsoCat_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b) : (CategoryTheory.Bicategory.rightUnitorNatIsoCat a b).hom.toNatTrans.app X = (CategoryTheory.Bicategory.rightUnitor X).hom
• CategoryTheory.Bicategory.rightUnitorNatIsoCat_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b) : (CategoryTheory.Bicategory.rightUnitorNatIsoCat a b).inv.toNatTrans.app X = (CategoryTheory.Bicategory.rightUnitor X).inv
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_map 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x✝ : B) {a b : Bᵒᵖ} (a✝ : a ⟶ b) {X✝ Y✝ : Opposite.unop a ⟶ x✝} (x✝¹ : X✝ ⟶ Y✝) : ((CategoryTheory.Bicategory.yoneda.obj x✝).map a✝).toFunctor.map x✝¹ = CategoryTheory.Bicategory.whiskerLeft a✝.unop x✝¹
• CategoryTheory.Bicategory.yoneda₀_mapId_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x) : ((CategoryTheory.Bicategory.yoneda₀ x).mapId a).hom.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).hom
• CategoryTheory.Bicategory.yoneda₀_mapId_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x) : ((CategoryTheory.Bicategory.yoneda₀ x).mapId a).inv.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).inv
• CategoryTheory.Bicategory.postcomposing₂_map_as_app_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) {X✝ Y✝ : a ⟶ b} (η : X✝ ⟶ Y✝) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : (((CategoryTheory.Bicategory.postcomposing₂ a b).map η).as.app x).toNatTrans.app x✝ = CategoryTheory.Bicategory.whiskerLeft x✝ η
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x✝ : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x✝) : ((CategoryTheory.Bicategory.yoneda.obj x✝).mapId a).hom.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).hom
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapId_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x✝ : B) (a : Bᵒᵖ) (X : Opposite.unop a ⟶ x✝) : ((CategoryTheory.Bicategory.yoneda.obj x✝).mapId a).inv.toNatTrans.app X = (CategoryTheory.Bicategory.leftUnitor X).inv
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_as_app_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f✝ g✝ : a ⟶ b} (a✝ : f✝ ⟶ g✝) (x : Bᵒᵖ) (x✝ : Opposite.unop x ⟶ a) : ((CategoryTheory.Bicategory.yoneda.map₂ a✝).as.app x).toNatTrans.app x✝ = CategoryTheory.Bicategory.whiskerLeft x✝ a✝
• CategoryTheory.Bicategory.yoneda₀_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x : B) {a b : Bᵒᵖ} {f✝ g✝ : a ⟶ b} (a✝ : f✝ ⟶ g✝) (x✝ : Opposite.unop a ⟶ x) : ((CategoryTheory.Bicategory.yoneda₀ x).map₂ a✝).toNatTrans.app x✝ = CategoryTheory.Bicategory.whiskerRight a✝.unop2 x✝
• CategoryTheory.Bicategory.associatorNatIsoRightCat_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d) : (CategoryTheory.Bicategory.associatorNatIsoRightCat f g d).hom.toNatTrans.app X = (CategoryTheory.Bicategory.associator f g X).hom
• CategoryTheory.Bicategory.associatorNatIsoRightCat_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d) : (CategoryTheory.Bicategory.associatorNatIsoRightCat f g d).inv.toNatTrans.app X = (CategoryTheory.Bicategory.associator f g X).inv
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x✝ : B) {a b : Bᵒᵖ} {f✝ g✝ : a ⟶ b} (a✝ : f✝ ⟶ g✝) (x✝¹ : Opposite.unop a ⟶ x✝) : ((CategoryTheory.Bicategory.yoneda.obj x✝).map₂ a✝).toNatTrans.app x✝¹ = CategoryTheory.Bicategory.whiskerRight a✝.unop2 x✝¹
• CategoryTheory.Bicategory.associatorNatIsoLeftCat_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a : B) {b c d : B} (g : b ⟶ c) (h : c ⟶ d) (X : ↑(CategoryTheory.Cat.of (a ⟶ b))) : (CategoryTheory.Bicategory.associatorNatIsoLeftCat a g h).hom.toNatTrans.app X = (CategoryTheory.Bicategory.associator X g h).hom
• CategoryTheory.Bicategory.associatorNatIsoLeftCat_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a : B) {b c d : B} (g : b ⟶ c) (h : c ⟶ d) (X : ↑(CategoryTheory.Cat.of (a ⟶ b))) : (CategoryTheory.Bicategory.associatorNatIsoLeftCat a g h).inv.toNatTrans.app X = (CategoryTheory.Bicategory.associator X g h).inv
• CategoryTheory.Bicategory.yoneda₀_mapComp_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x : B) {a✝ b✝ c✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (X : Opposite.unop a✝ ⟶ x) : ((CategoryTheory.Bicategory.yoneda₀ x).mapComp f g).hom.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop f.unop X).hom
• CategoryTheory.Bicategory.yoneda₀_mapComp_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x : B) {a✝ b✝ c✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (X : Opposite.unop a✝ ⟶ x) : ((CategoryTheory.Bicategory.yoneda₀ x).mapComp f g).inv.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop f.unop X).inv
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x✝ : B) {a✝ b✝ c✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (X : Opposite.unop a✝ ⟶ x✝) : ((CategoryTheory.Bicategory.yoneda.obj x✝).mapComp f g).hom.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop f.unop X).hom
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_mapComp_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (x✝ : B) {a✝ b✝ c✝ : Bᵒᵖ} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (X : Opposite.unop a✝ ⟶ x✝) : ((CategoryTheory.Bicategory.yoneda.obj x✝).mapComp f g).inv.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop f.unop X).inv
• CategoryTheory.Bicategory.associatorNatIsoMiddleCat_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) (X : ↑(CategoryTheory.Cat.of (b ⟶ c))) : (CategoryTheory.Bicategory.associatorNatIsoMiddleCat f h).hom.toNatTrans.app X = (CategoryTheory.Bicategory.associator f X h).hom
• CategoryTheory.Bicategory.associatorNatIsoMiddleCat_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) (X : ↑(CategoryTheory.Cat.of (b ⟶ c))) : (CategoryTheory.Bicategory.associatorNatIsoMiddleCat f h).inv.toNatTrans.app X = (CategoryTheory.Bicategory.associator f X h).inv
• CategoryTheory.Bicategory.postcomp₂_naturality_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) {a✝ b✝ : Bᵒᵖ} (g : a✝ ⟶ b✝) (X : ↑(CategoryTheory.Cat.of (Opposite.unop a✝ ⟶ a))) : ((CategoryTheory.Bicategory.postcomp₂ f).naturality g).hom.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop X f).hom
• CategoryTheory.Bicategory.postcomp₂_naturality_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) {a✝ b✝ : Bᵒᵖ} (g : a✝ ⟶ b✝) (X : ↑(CategoryTheory.Cat.of (Opposite.unop a✝ ⟶ a))) : ((CategoryTheory.Bicategory.postcomp₂ f).naturality g).inv.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop X f).inv
• CategoryTheory.Bicategory.postcomposing₂_obj_naturality_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b) {a✝ b✝ : Bᵒᵖ} (g : a✝ ⟶ b✝) (X : ↑(CategoryTheory.Cat.of (Opposite.unop a✝ ⟶ a))) : (((CategoryTheory.Bicategory.postcomposing₂ a b).obj f).naturality g).hom.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop X f).hom
• CategoryTheory.Bicategory.postcomposing₂_obj_naturality_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (f : a ⟶ b) {a✝ b✝ : Bᵒᵖ} (g : a✝ ⟶ b✝) (X : ↑(CategoryTheory.Cat.of (Opposite.unop a✝ ⟶ a))) : (((CategoryTheory.Bicategory.postcomposing₂ a b).obj f).naturality g).inv.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop X f).inv
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (a✝ : a ⟶ b) {a✝¹ b✝ : Bᵒᵖ} (g : a✝¹ ⟶ b✝) (X : ↑(CategoryTheory.Cat.of (Opposite.unop a✝¹ ⟶ a))) : ((CategoryTheory.Bicategory.yoneda.map a✝).naturality g).hom.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop X a✝).hom
• CategoryTheory.Bicategory.yoneda_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_naturality_inv_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (a✝ : a ⟶ b) {a✝¹ b✝ : Bᵒᵖ} (g : a✝¹ ⟶ b✝) (X : ↑(CategoryTheory.Cat.of (Opposite.unop a✝¹ ⟶ a))) : ((CategoryTheory.Bicategory.yoneda.map a✝).naturality g).inv.toNatTrans.app X = (CategoryTheory.Bicategory.associator g.unop X a✝).inv
• CategoryTheory.Bicategory.yoneda_mapId_hom_as_app_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a : B) (a✝ : Bᵒᵖ) (X : Opposite.unop a✝ ⟶ a) : ((CategoryTheory.Bicategory.yoneda.mapId a).hom.as.app a✝).toNatTrans.app X = (CategoryTheory.Bicategory.rightUnitor X).hom
• CategoryTheory.Bicategory.yoneda_mapId_inv_as_app_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] (a : B) (a✝ : Bᵒᵖ) (X : Opposite.unop a✝ ⟶ a) : ((CategoryTheory.Bicategory.yoneda.mapId a).inv.as.app a✝).toNatTrans.app X = (CategoryTheory.Bicategory.rightUnitor X).inv
• CategoryTheory.Bicategory.yoneda_mapComp_hom_as_app_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (a : Bᵒᵖ) (X : ↑(CategoryTheory.Cat.of (Opposite.unop a ⟶ a✝))) : ((CategoryTheory.Bicategory.yoneda.mapComp f g).hom.as.app a).toNatTrans.app X = (CategoryTheory.Bicategory.associator X f g).inv
• CategoryTheory.Bicategory.yoneda_mapComp_inv_as_app_toNatTrans_app 📋 Mathlib.CategoryTheory.Bicategory.Yoneda
  {B : Type u} [CategoryTheory.Bicategory B] {a✝ b✝ c✝ : B} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) (a : Bᵒᵖ) (X : ↑(CategoryTheory.Cat.of (Opposite.unop a ⟶ a✝))) : ((CategoryTheory.Bicategory.yoneda.mapComp f g).inv.as.app a).toNatTrans.app X = (CategoryTheory.Bicategory.associator X f g).hom
• CategoryTheory.Cat.HasLimits.limitCone_π_app 📋 Mathlib.CategoryTheory.Category.Cat.Limit
  {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat) (j : J) : (CategoryTheory.Cat.HasLimits.limitCone F).π.app j = { obj := ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Cat.objects) j)), map := fun {X Y} f => (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (CategoryTheory.Cat.HasLimits.homDiagram X Y) j)) f, map_id := ⋯, map_comp := ⋯ }.toCatHom
• CategoryTheory.Cat.opFunctor_obj 📋 Mathlib.CategoryTheory.Category.Cat.Op
  (C : CategoryTheory.Cat) : CategoryTheory.Cat.opFunctor.obj C = CategoryTheory.Cat.of (↑C)ᵒᵖ
• CategoryTheory.Cat.opFunctor_map 📋 Mathlib.CategoryTheory.Category.Cat.Op
  {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) : CategoryTheory.Cat.opFunctor.map F = F.toFunctor.op.toCatHom
• CategoryTheory.Grpd.freeForgetAdjunction_unit_app 📋 Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
  {C : Type u} [CategoryTheory.Category.{u, u} C] : (CategoryTheory.Grpd.freeForgetAdjunction.unit.app (CategoryTheory.Cat.of C)).toFunctor = CategoryTheory.FreeGroupoid.of C
• CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_apply 📋 Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
  {C : Type u} [CategoryTheory.Category.{u, u} C] {D : Type u} [CategoryTheory.Groupoid D] (F : CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) D) : ((CategoryTheory.Grpd.freeForgetAdjunction.homEquiv (CategoryTheory.Cat.of C) (CategoryTheory.Grpd.of D)) F).toFunctor = (CategoryTheory.FreeGroupoid.of C).comp F
• CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_symm_apply 📋 Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
  {C : Type u} [CategoryTheory.Category.{u, u} C] {D : Type u} [CategoryTheory.Groupoid D] (F : CategoryTheory.Functor C D) : (CategoryTheory.Grpd.freeForgetAdjunction.homEquiv (CategoryTheory.Cat.of C) (CategoryTheory.Grpd.of D)).symm F.toCatHom = (CategoryTheory.FreeGroupoid.map F).comp (CategoryTheory.FreeGroupoid.lift (CategoryTheory.Functor.id D))
• CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj 📋 Mathlib.CategoryTheory.Join.Pseudofunctor
  (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) (X : CategoryTheory.Join (↑X✝) D) : ((CategoryTheory.Join.pseudofunctorLeft D).map F).toFunctor.obj X = match X with | CategoryTheory.Join.left x => CategoryTheory.Join.left (F.toFunctor.obj x) | CategoryTheory.Join.right x => CategoryTheory.Join.right x
• CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_toFunctor_obj 📋 Mathlib.CategoryTheory.Join.Pseudofunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : CategoryTheory.Cat} (F : X✝ ⟶ Y✝) (X : CategoryTheory.Join C ↑X✝) : ((CategoryTheory.Join.pseudofunctorRight C).map F).toFunctor.obj X = match X with | CategoryTheory.Join.left x => CategoryTheory.Join.left x | CategoryTheory.Join.right x => CategoryTheory.Join.right (F.toFunctor.obj x)
• CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app 📋 Mathlib.CategoryTheory.Join.Pseudofunctor
  (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] {a✝ b✝ : CategoryTheory.Cat} {f✝ g✝ : a✝ ⟶ b✝} (x✝ : f✝ ⟶ g✝) (x : CategoryTheory.Join (↑a✝) D) : ((CategoryTheory.Join.pseudofunctorLeft D).map₂ x✝).toNatTrans.app x = match x with | CategoryTheory.Join.left x => (CategoryTheory.Join.inclLeft (↑b✝) D).map (x✝.toNatTrans.app x) | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x)
• CategoryTheory.Join.pseudofunctorRight_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app 📋 Mathlib.CategoryTheory.Join.Pseudofunctor
  (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {a✝ b✝ : CategoryTheory.Cat} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) (x : CategoryTheory.Join C ↑a✝) : ((CategoryTheory.Join.pseudofunctorRight C).map₂ f).toNatTrans.app x = match x with | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x) | CategoryTheory.Join.right x => (CategoryTheory.Join.inclRight C ↑b✝).map (f.toNatTrans.app x)
• CategoryTheory.Join.pseudofunctorLeft_mapId_hom_toNatTrans_app 📋 Mathlib.CategoryTheory.Join.Pseudofunctor
  (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] (D✝ : CategoryTheory.Cat) (x : CategoryTheory.Join (↑D✝) D) : ((CategoryTheory.Join.pseudofunctorLeft D).mapId D✝).hom.toNatTrans.app x = match x with | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x) | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c