Loogle!

Result

Found 3313 declarations mentioning CategoryTheory.Discrete. Of these, only the first 200 are shown.

• CategoryTheory.Discrete 📋 Mathlib.CategoryTheory.Discrete.Basic
  (α : Type u₁) : Type u₁
• CategoryTheory.discreteCategory 📋 Mathlib.CategoryTheory.Discrete.Basic
  (α : Type u₁) : CategoryTheory.SmallCategory (CategoryTheory.Discrete α)
• CategoryTheory.Discrete.as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (self : CategoryTheory.Discrete α) : α
• CategoryTheory.Discrete.mk 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (as : α) : CategoryTheory.Discrete α
• CategoryTheory.discreteEquiv 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} : CategoryTheory.Discrete α ≃ α
• CategoryTheory.instDecidableEqDiscrete 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} [DecidableEq α] : DecidableEq (CategoryTheory.Discrete α)
• CategoryTheory.Discrete.instInhabited 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} [Inhabited α] : Inhabited (CategoryTheory.Discrete α)
• CategoryTheory.Discrete.instSubsingleton 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} [Subsingleton α] : Subsingleton (CategoryTheory.Discrete α)
• CategoryTheory.Discrete.instUnique 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} [Unique α] : Unique (CategoryTheory.Discrete α)
• CategoryTheory.Discrete.isDiscrete 📋 Mathlib.CategoryTheory.Discrete.Basic
  (C : Type u_1) : CategoryTheory.IsDiscrete (CategoryTheory.Discrete C)
• CategoryTheory.Discrete.as_bijective 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u_1} : Function.Bijective CategoryTheory.Discrete.as
• CategoryTheory.Discrete.mk_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (X : CategoryTheory.Discrete α) : { as := X.as } = X
• CategoryTheory.Discrete.functor 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) : CategoryTheory.Functor (CategoryTheory.Discrete I) C
• CategoryTheory.Discrete.equivOfEquivalence 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {β : Type u₂} (h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β) : α ≃ β
• CategoryTheory.Discrete.equivalence 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : CategoryTheory.Discrete I ≌ CategoryTheory.Discrete J
• CategoryTheory.Discrete.forall 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u_1} {p : CategoryTheory.Discrete α → Prop} : (∀ (a : CategoryTheory.Discrete α), p a) ↔ ∀ (a' : α), p { as := a' }
• CategoryTheory.Discrete.opposite 📋 Mathlib.CategoryTheory.Discrete.Basic
  (α : Type u₁) : (CategoryTheory.Discrete α)ᵒᵖ ≌ CategoryTheory.Discrete α
• CategoryTheory.Discrete.eqToIso' 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {a b : α} (h : a = b) : { as := a } ≅ { as := b }
• CategoryTheory.Discrete.ext 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {x y : CategoryTheory.Discrete α} (as : x.as = y.as) : x = y
• CategoryTheory.Discrete.exists 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u_1} {p : CategoryTheory.Discrete α → Prop} : (∃ a, p a) ↔ ∃ a', p { as := a' }
• CategoryTheory.Discrete.ext_iff 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {x y : CategoryTheory.Discrete α} : x = y ↔ x.as = y.as
• CategoryTheory.Discrete.instSubsingletonDiscreteHom 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (X Y : CategoryTheory.Discrete α) : Subsingleton (X ⟶ Y)
• CategoryTheory.Discrete.eqToIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {X Y : CategoryTheory.Discrete α} (h : X.as = Y.as) : X ≅ Y
• CategoryTheory.Discrete.eqToHom' 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {a b : α} (h : a = b) : { as := a } ⟶ { as := b }
• CategoryTheory.Discrete.id_def' 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (X : α) : { eq := ⋯ } = CategoryTheory.CategoryStruct.id { as := X }
• CategoryTheory.Discrete.eqToHom 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {X Y : CategoryTheory.Discrete α} (h : X.as = Y.as) : X ⟶ Y
• CategoryTheory.Discrete.eq_of_hom 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {X Y : CategoryTheory.Discrete α} (i : X ⟶ Y) : X.as = Y.as
• CategoryTheory.Discrete.functor_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (i : I) : (CategoryTheory.Discrete.functor F).obj { as := i } = F i
• CategoryTheory.Discrete.instIsIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {i j : CategoryTheory.Discrete I} (f : i ⟶ j) : CategoryTheory.IsIso f
• CategoryTheory.piEquivalenceFunctorDiscrete 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : J → C ≌ CategoryTheory.Functor (CategoryTheory.Discrete J) C
• CategoryTheory.Discrete.functor_obj_eq_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functor F).obj X = F X.as
• CategoryTheory.Discrete.range_functor 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u_1} (X : I → C) : Set.range (CategoryTheory.Discrete.functor X).obj = Set.range X
• CategoryTheory.discreteEquiv_apply 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (self : CategoryTheory.Discrete α) : CategoryTheory.discreteEquiv self = self.as
• CategoryTheory.Discrete.id_def 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (X : CategoryTheory.Discrete α) : { eq := ⋯ } = CategoryTheory.CategoryStruct.id X
• CategoryTheory.discreteEquiv_symm_apply_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} (as : α) : (CategoryTheory.discreteEquiv.symm as).as = as
• CategoryTheory.Discrete.opposite_inverse_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  (α : Type u₁) (a✝ : CategoryTheory.Discrete α) : (CategoryTheory.Discrete.opposite α).inverse.obj a✝ = Opposite.op a✝
• CategoryTheory.Discrete.opposite_functor_obj_as 📋 Mathlib.CategoryTheory.Discrete.Basic
  (α : Type u₁) (X : (CategoryTheory.Discrete α)ᵒᵖ) : ((CategoryTheory.Discrete.opposite α).functor.obj X).as = (Opposite.unop X).as
• CategoryTheory.Discrete.natIsoFunctor 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} : F ≅ CategoryTheory.Discrete.functor (F.obj ∘ CategoryTheory.Discrete.mk)
• CategoryTheory.Discrete.hom_eq 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {X Y : CategoryTheory.Discrete α} {f g : X ⟶ Y} : f = g
• CategoryTheory.Discrete.functor_ext 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {G F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (h : ∀ (i : I), G.obj { as := i } = F.obj { as := i }) : G = F
• CategoryTheory.Discrete.functor_ext_iff 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {G F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} : G = F ↔ ∀ (i : I), G.obj { as := i } = F.obj { as := i }
• CategoryTheory.Discrete.equivalence_functor 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (CategoryTheory.Discrete.equivalence e).functor = CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑e)
• CategoryTheory.Discrete.natIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i) : F ≅ G
• CategoryTheory.Discrete.compNatIsoDiscrete 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D) : (CategoryTheory.Discrete.functor F).comp G ≅ CategoryTheory.Discrete.functor (G.obj ∘ F)
• CategoryTheory.Discrete.equivalence_inverse 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (CategoryTheory.Discrete.equivalence e).inverse = CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑e.symm)
• CategoryTheory.Discrete.functorComp 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) : CategoryTheory.Discrete.functor (f ∘ g) ≅ (CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ g)).comp (CategoryTheory.Discrete.functor f)
• CategoryTheory.piEquivalenceFunctorDiscrete_functor_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (F : J → C) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.obj F = CategoryTheory.Discrete.functor F
• CategoryTheory.Discrete.equivOfEquivalence_apply 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {β : Type u₂} (h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β) (a✝ : α) : (CategoryTheory.Discrete.equivOfEquivalence h) a✝ = (CategoryTheory.Discrete.as ∘ h.functor.obj ∘ CategoryTheory.Discrete.mk) a✝
• CategoryTheory.Discrete.equivOfEquivalence_symm_apply 📋 Mathlib.CategoryTheory.Discrete.Basic
  {α : Type u₁} {β : Type u₂} (h : CategoryTheory.Discrete α ≌ CategoryTheory.Discrete β) (a✝ : β) : (CategoryTheory.Discrete.equivOfEquivalence h).symm a✝ = (CategoryTheory.Discrete.as ∘ h.inverse.obj ∘ CategoryTheory.Discrete.mk) a✝
• CategoryTheory.piEquivalenceFunctorDiscrete_inverse_obj 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) (j : J) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).inverse.obj F j = F.obj { as := j }
• CategoryTheory.Discrete.functor_map_id 📋 Mathlib.CategoryTheory.Discrete.Basic
  {J : Type v₁} {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete J) C) {j : CategoryTheory.Discrete J} (f : j ⟶ j) : F.map f = CategoryTheory.CategoryStruct.id (F.obj j)
• CategoryTheory.Discrete.natTrans 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ⟶ G.obj i) : F ⟶ G
• CategoryTheory.Discrete.functor_map 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} (F : I → C) {i : CategoryTheory.Discrete I} (f : i ⟶ i) : (CategoryTheory.Discrete.functor F).map f = CategoryTheory.CategoryStruct.id (F i.as)
• CategoryTheory.Discrete.natIso_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i) (i : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.natIso f).app i = f i
• CategoryTheory.Discrete.natTrans_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ⟶ G.obj i) (i : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.natTrans f).app i = f i
• CategoryTheory.Discrete.instIsIsoFunctorNatTrans 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u_1} {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ⟶ G.obj i) [∀ (i : CategoryTheory.Discrete I), CategoryTheory.IsIso (f i)] : CategoryTheory.IsIso (CategoryTheory.Discrete.natTrans f)
• CategoryTheory.Discrete.natIso_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.natIso f).hom.app X = (f X).hom
• CategoryTheory.Discrete.natIso_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F G : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (f : (i : CategoryTheory.Discrete I) → F.obj i ≅ G.obj i) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.natIso f).inv.app X = (f X).inv
• CategoryTheory.piEquivalenceFunctorDiscrete_unitIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.piEquivalenceFunctorDiscrete J C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (J → C))
• CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} (j : J) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.comp ((CategoryTheory.evaluation (CategoryTheory.Discrete J) C).obj { as := j }) ≅ CategoryTheory.Pi.eval (fun a => C) j
• CategoryTheory.Discrete.natIsoFunctor_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (X : CategoryTheory.Discrete I) : CategoryTheory.Discrete.natIsoFunctor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.Discrete.natIsoFunctor_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {F : CategoryTheory.Functor (CategoryTheory.Discrete I) C} (X : CategoryTheory.Discrete I) : CategoryTheory.Discrete.natIsoFunctor.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
• CategoryTheory.piEquivalenceFunctorDiscrete_functor_map 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : J → C} (f : X✝ ⟶ Y✝) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).functor.map f = CategoryTheory.Discrete.natTrans fun j => f j.as
• CategoryTheory.piEquivalenceFunctorDiscrete_inverse_map 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] {X✝ Y✝ : CategoryTheory.Functor (CategoryTheory.Discrete J) C} (f : X✝ ⟶ Y✝) (j : J) : (CategoryTheory.piEquivalenceFunctorDiscrete J C).inverse.map f j = f.app { as := j }
• CategoryTheory.Discrete.compNatIsoDiscrete_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.compNatIsoDiscrete F G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj (F X.as))
• CategoryTheory.Discrete.compNatIsoDiscrete_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : I → C) (G : CategoryTheory.Functor C D) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.compNatIsoDiscrete F G).inv.app X = CategoryTheory.CategoryStruct.id (G.obj (F X.as))
• CategoryTheory.Discrete.functorComp_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functorComp f g).hom.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
• CategoryTheory.Discrete.functorComp_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {I : Type u₁} {J : Type u₁'} (f : J → C) (g : I → J) (X : CategoryTheory.Discrete I) : (CategoryTheory.Discrete.functorComp f g).inv.app X = CategoryTheory.CategoryStruct.id (f (g X.as))
• CategoryTheory.Discrete.equivalence_counitIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (CategoryTheory.Discrete.equivalence e).counitIso = CategoryTheory.Discrete.natIso fun j => CategoryTheory.eqToIso ⋯
• CategoryTheory.Discrete.equivalence_unitIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  {I : Type u₁} {J : Type u₂} (e : I ≃ J) : (CategoryTheory.Discrete.equivalence e).unitIso = CategoryTheory.Discrete.natIso fun i => CategoryTheory.eqToIso ⋯
• CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso_hom_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} (j : J) (X : J → C) : (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C j).hom.app X = CategoryTheory.CategoryStruct.id (X j)
• CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso_inv_app 📋 Mathlib.CategoryTheory.Discrete.Basic
  (C : Type u_1) [CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} (j : J) (X : J → C) : (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C j).inv.app X = CategoryTheory.CategoryStruct.id (X j)
• CategoryTheory.piEquivalenceFunctorDiscrete_counitIso 📋 Mathlib.CategoryTheory.Discrete.Basic
  (J : Type u₂) (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] : (CategoryTheory.piEquivalenceFunctorDiscrete J C).counitIso = CategoryTheory.NatIso.ofComponents (fun F => CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.Iso.refl ((({ obj := fun F j => F.obj { as := j }, map := fun {X Y} f j => f.app { as := j }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun F => CategoryTheory.Discrete.functor F, map := fun {X Y} f => CategoryTheory.Discrete.natTrans fun j => f j.as, map_id := ⋯, map_comp := ⋯ }).obj F).obj x)) ⋯) ⋯
• CategoryTheory.prod.leftInverseUnitor 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1} × C)
• CategoryTheory.prod.leftUnitor 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{w + 1} × C) C
• CategoryTheory.prod.leftUnitorEquivalence 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Discrete PUnit.{w + 1} × C ≌ C
• CategoryTheory.prod.rightInverseUnitor 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor C (C × CategoryTheory.Discrete PUnit.{w + 1})
• CategoryTheory.prod.rightUnitor 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : CategoryTheory.Functor (C × CategoryTheory.Discrete PUnit.{w + 1}) C
• CategoryTheory.prod.rightUnitorEquivalence 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : C × CategoryTheory.Discrete PUnit.{w + 1} ≌ C
• CategoryTheory.prod.leftUnitor_isEquivalence 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitor C).IsEquivalence
• CategoryTheory.prod.rightUnitor_isEquivalence 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitor C).IsEquivalence
• CategoryTheory.prod.leftUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Discrete PUnit.{w + 1} × C) : (CategoryTheory.prod.leftUnitor C).obj X = X.2
• CategoryTheory.prod.rightUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C × CategoryTheory.Discrete PUnit.{w + 1}) : (CategoryTheory.prod.rightUnitor C).obj X = X.1
• CategoryTheory.prod.leftInverseUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.prod.leftInverseUnitor C).obj X = ({ as := PUnit.unit }, X)
• CategoryTheory.prod.rightInverseUnitor_obj 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.prod.rightInverseUnitor C).obj X = (X, { as := PUnit.unit })
• CategoryTheory.prod.leftUnitorEquivalence_functor 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitorEquivalence C).functor = CategoryTheory.prod.leftUnitor C
• CategoryTheory.prod.leftUnitorEquivalence_inverse 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitorEquivalence C).inverse = CategoryTheory.prod.leftInverseUnitor C
• CategoryTheory.prod.rightUnitorEquivalence_functor 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitorEquivalence C).functor = CategoryTheory.prod.rightUnitor C
• CategoryTheory.prod.rightUnitorEquivalence_inverse 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitorEquivalence C).inverse = CategoryTheory.prod.rightInverseUnitor C
• CategoryTheory.prod.leftInverseUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.leftInverseUnitor C).map f = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id { as := PUnit.unit }) f
• CategoryTheory.prod.rightInverseUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.rightInverseUnitor C).map f = CategoryTheory.Prod.mkHom f (CategoryTheory.CategoryStruct.id { as := PUnit.unit })
• CategoryTheory.prod.leftUnitorEquivalence_counitIso 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitorEquivalence C).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.prod.leftInverseUnitor C).comp (CategoryTheory.prod.leftUnitor C))
• CategoryTheory.prod.rightUnitorEquivalence_counitIso 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitorEquivalence C).counitIso = CategoryTheory.Iso.refl ((CategoryTheory.prod.rightInverseUnitor C).comp (CategoryTheory.prod.rightUnitor C))
• CategoryTheory.prod.leftUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : CategoryTheory.Discrete PUnit.{w + 1} × C} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.leftUnitor C).map f = f.2
• CategoryTheory.prod.rightUnitor_map 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] {X✝ Y✝ : C × CategoryTheory.Discrete PUnit.{w + 1}} (f : X✝ ⟶ Y✝) : (CategoryTheory.prod.rightUnitor C).map f = f.1
• CategoryTheory.prod.leftUnitorEquivalence_unitIso 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.leftUnitorEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Discrete PUnit.{w + 1} × C))
• CategoryTheory.prod.rightUnitorEquivalence_unitIso 📋 Mathlib.CategoryTheory.Products.Unitor
  (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.prod.rightUnitorEquivalence C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (C × CategoryTheory.Discrete PUnit.{w + 1}))
• CategoryTheory.Comma.toIdPUnitEquiv 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})) : CategoryTheory.Comma L R ≌ B
• CategoryTheory.Comma.toPUnitIdEquiv 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})) : CategoryTheory.Comma L R ≌ A
• CategoryTheory.Comma.equivProd 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) : CategoryTheory.Comma L R ≌ A × B
• CategoryTheory.Comma.fromProd 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) : CategoryTheory.Functor (A × B) (CategoryTheory.Comma L R)
• CategoryTheory.Comma.fromProd_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.fromProd L R).obj X).left = X.1
• CategoryTheory.Comma.fromProd_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.fromProd L R).obj X).right = X.2
• CategoryTheory.Comma.toIdPUnitEquiv_functor_iso 📋 Mathlib.CategoryTheory.Comma.Basic
  {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {L : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) (CategoryTheory.Discrete PUnit.{u_2 + 1})} {R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_2 + 1})} : (CategoryTheory.Comma.toIdPUnitEquiv L R).functor = CategoryTheory.Comma.snd L R
• CategoryTheory.Comma.toPUnitIdEquiv_functor_iso 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})} {R : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_2 + 1}) (CategoryTheory.Discrete PUnit.{u_1 + 1})} : (CategoryTheory.Comma.toPUnitIdEquiv L R).functor = CategoryTheory.Comma.fst L R
• CategoryTheory.Comma.equivProd_inverse_obj_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.equivProd L R).inverse.obj X).left = X.1
• CategoryTheory.Comma.equivProd_inverse_obj_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.equivProd L R).inverse.obj X).right = X.2
• CategoryTheory.Comma.equivProd_functor_obj 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (a : CategoryTheory.Comma L R) : (CategoryTheory.Comma.equivProd L R).functor.obj a = (a.left, a.right)
• CategoryTheory.Comma.fromProd_obj_hom 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : ((CategoryTheory.Comma.fromProd L R).obj X).hom = CategoryTheory.Discrete.eqToHom ⋯
• CategoryTheory.Comma.fromProd_map_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y) : ((CategoryTheory.Comma.fromProd L R).map f).left = f.1
• CategoryTheory.Comma.fromProd_map_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y) : ((CategoryTheory.Comma.fromProd L R).map f).right = f.2
• CategoryTheory.Comma.equivProd_inverse_map_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y) : ((CategoryTheory.Comma.equivProd L R).inverse.map f).left = f.1
• CategoryTheory.Comma.equivProd_inverse_map_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X Y : A × B} (f : X ⟶ Y) : ((CategoryTheory.Comma.equivProd L R).inverse.map f).right = f.2
• CategoryTheory.Comma.equivProd_functor_map 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) {X✝ Y✝ : CategoryTheory.Comma L R} (f : X✝ ⟶ Y✝) : (CategoryTheory.Comma.equivProd L R).functor.map f = CategoryTheory.Prod.mkHom f.left f.right
• CategoryTheory.Comma.equivProd_unitIso_hom_app_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.equivProd L R).unitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
• CategoryTheory.Comma.equivProd_unitIso_hom_app_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.equivProd L R).unitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
• CategoryTheory.Comma.equivProd_unitIso_inv_app_left 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.equivProd L R).unitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
• CategoryTheory.Comma.equivProd_unitIso_inv_app_right 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : CategoryTheory.Comma L R) : ((CategoryTheory.Comma.equivProd L R).unitIso.inv.app X).right = CategoryTheory.CategoryStruct.id X.right
• CategoryTheory.Comma.equivProd_counitIso_hom_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : (CategoryTheory.Comma.equivProd L R).counitIso.hom.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.Comma.equivProd_counitIso_inv_app 📋 Mathlib.CategoryTheory.Comma.Basic
  {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (X : A × B) : (CategoryTheory.Comma.equivProd L R).counitIso.inv.app X = CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X.1) (CategoryTheory.CategoryStruct.id X.2)
• CategoryTheory.Arrow.discreteEquiv 📋 Mathlib.CategoryTheory.Comma.Arrow
  (S : Type u) : CategoryTheory.Arrow (CategoryTheory.Discrete S) ≃ S
• CategoryTheory.instIsGroupoidDiscrete 📋 Mathlib.CategoryTheory.Groupoid
  {I : Type u_1} : CategoryTheory.IsGroupoid (CategoryTheory.Discrete I)
• CategoryTheory.Limits.inhabitedCocone 📋 Mathlib.CategoryTheory.Limits.Cones
  {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C) : Inhabited (CategoryTheory.Limits.Cocone F)
• CategoryTheory.Limits.inhabitedCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C) : Inhabited (CategoryTheory.Limits.Cone F)
• CategoryTheory.typeToCat_obj 📋 Mathlib.CategoryTheory.Category.Cat
  (X : Type u) : CategoryTheory.typeToCat.obj X = CategoryTheory.Cat.of (CategoryTheory.Discrete X)
• 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.instSmallDiscrete 📋 Mathlib.CategoryTheory.EssentiallySmall
  (C : Type u) [Small.{w, u} C] : Small.{w, u} (CategoryTheory.Discrete C)
• CategoryTheory.Discrete.essentiallySmallOfSmall 📋 Mathlib.CategoryTheory.EssentiallySmall
  {α : Type u} [Small.{w, u} α] : CategoryTheory.EssentiallySmall.{w, u, u} (CategoryTheory.Discrete α)
• CategoryTheory.Limits.colimitCoconeOfUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : CategoryTheory.Limits.ColimitCocone (CategoryTheory.Discrete.functor f)
• CategoryTheory.Limits.limitConeOfUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor f)
• CategoryTheory.Limits.hasCoproducts_of_colimit_cofans 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (cf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Cofan f) (cf_isColimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsColimit (cf f)) : CategoryTheory.Limits.HasCoproducts C
• CategoryTheory.Limits.hasProducts_of_limit_fans 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] (lf : {J : Type w} → (f : J → C) → CategoryTheory.Limits.Fan f) (lf_isLimit : {J : Type w} → (f : J → C) → CategoryTheory.Limits.IsLimit (lf f)) : CategoryTheory.Limits.HasProducts C
• CategoryTheory.Limits.Cofan.inj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (p : CategoryTheory.Limits.Cofan f) (j : β) : f j ⟶ p.pt
• CategoryTheory.Limits.Fan.proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (p : CategoryTheory.Limits.Fan f) (j : β) : p.pt ⟶ f j
• CategoryTheory.Limits.Pi.cone 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : CategoryTheory.Limits.Cone X
• CategoryTheory.Limits.Sigma.cocone 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] : CategoryTheory.Limits.Cocone X
• CategoryTheory.Limits.coproductIsCoproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) [CategoryTheory.Limits.HasCoproduct f] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (∐ f) (CategoryTheory.Limits.Sigma.ι f))
• CategoryTheory.Limits.productIsProduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : β → C) [CategoryTheory.Limits.HasProduct f] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (∏ᶜ f) (CategoryTheory.Limits.Pi.π f))
• CategoryTheory.Limits.Cofan.isColimitMkOfUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y) (J : Type u_1) [Unique J] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk Y fun x => e.hom)
• CategoryTheory.Limits.Cofan.mk_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) : (CategoryTheory.Limits.Cofan.mk P p).pt = P
• CategoryTheory.Limits.Fan.isLimitMkOfUnique 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y) (J : Type u_1) [Unique J] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk X fun x => e.hom)
• CategoryTheory.Limits.Fan.mk_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) : (CategoryTheory.Limits.Fan.mk P p).pt = P
• CategoryTheory.Limits.coproductIsCoproduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Sigma.cocone X)
• CategoryTheory.Limits.productIsProduct' 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Pi.cone X)
• CategoryTheory.Limits.colimitCoconeOfUnique_cocone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.colimitCoconeOfUnique f).cocone.pt = f default
• CategoryTheory.Limits.limitConeOfUnique_cone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : β → C) : (CategoryTheory.Limits.limitConeOfUnique f).cone.pt = f default
• CategoryTheory.Limits.Cofan.IsColimit.desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) : c.pt ⟶ A
• CategoryTheory.Limits.Fan.IsLimit.lift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) : A ⟶ c.pt
• CategoryTheory.Limits.Pi.mapIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) : ∏ᶜ f ≅ ∏ᶜ g
• CategoryTheory.Limits.Sigma.mapIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) : ∐ f ≅ ∐ g
• CategoryTheory.Limits.Pi.cone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Pi.cone X).pt = ∏ᶜ fun j => X.obj { as := j }
• CategoryTheory.Limits.Sigma.cocone_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Sigma.cocone X).pt = ∐ fun j => X.obj { as := j }
• CategoryTheory.Limits.cofan_mk_inj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) : (CategoryTheory.Limits.Cofan.mk P p).inj = p
• CategoryTheory.Limits.fan_mk_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) : (CategoryTheory.Limits.Fan.mk P p).proj = p
• CategoryTheory.Limits.Pi.isoLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] : (∏ᶜ fun j => X.obj { as := j }) ≅ CategoryTheory.Limits.limit X
• CategoryTheory.Limits.Sigma.isoColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasColimit X] : (∐ fun j => X.obj { as := j }) ≅ CategoryTheory.Limits.colimit X
• CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasCoproduct f] (c : CategoryTheory.Limits.Cofan f) [hc : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)] : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.Fan.isLimitOfIsIsoPiLift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] (c : CategoryTheory.Limits.Fan f) [hc : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)] : CategoryTheory.Limits.IsLimit c
• CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasCoproduct f] (c : CategoryTheory.Limits.Cofan f) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.desc c.inj)
• CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} [CategoryTheory.Limits.HasProduct f] (c : CategoryTheory.Limits.Fan f) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ CategoryTheory.IsIso (CategoryTheory.Limits.Pi.lift c.proj)
• CategoryTheory.Limits.piEquivalenceFunctorDiscrete_functor_comp_colim 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] : (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.colim = CategoryTheory.Limits.Sigma.functor α
• CategoryTheory.Limits.Cofan.IsColimit.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) = f i
• CategoryTheory.Limits.Fan.IsLimit.fac 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc f) (c.proj i) = f i
• CategoryTheory.Limits.Cofan.mk_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) (X : CategoryTheory.Discrete β) : (CategoryTheory.Limits.Cofan.mk P p).ι.app X = p X.as
• CategoryTheory.Limits.Fan.mk_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) (X : CategoryTheory.Discrete β) : (CategoryTheory.Limits.Fan.mk P p).π.app X = p X.as
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompColim 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] : (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.Sigma.functor α
• CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  (α : Type w₂) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] : (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.Pi.functor α
• CategoryTheory.Limits.isColimitEquivCofanOfIsThin 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) : CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c.pt c.ι.app)
• CategoryTheory.Limits.isLimitEquivFanOfIsThin 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] [Quiver.IsThin C] {J : Type u_1} [CategoryTheory.Category.{v_1, u_1} J] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone K) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk c.pt c.π.app)
• CategoryTheory.Limits.Pi.map_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), CategoryTheory.IsIso (p b)] : CategoryTheory.IsIso (CategoryTheory.Limits.Pi.map p)
• CategoryTheory.Limits.Sigma.map_isIso 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), CategoryTheory.IsIso (p b)] : CategoryTheory.IsIso (CategoryTheory.Limits.Sigma.map p)
• CategoryTheory.Limits.Cofan.IsColimit.inj_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X} (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) : CategoryTheory.CategoryStruct.comp (c.inj i) (hc.desc d) = d.inj i
• CategoryTheory.Limits.Fan.IsLimit.lift_proj 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X} (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β) : CategoryTheory.CategoryStruct.comp (hc.lift d) (c.proj i) = d.proj i
• CategoryTheory.Limits.Cofan.isColimitEquivOfEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) {f : γ → C} (c : CategoryTheory.Limits.Cofan f) : CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk c.pt fun i => c.inj (ε i))
• CategoryTheory.Limits.Fan.isLimitEquivOfEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) {f : γ → C} (c : CategoryTheory.Limits.Fan f) : CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk c.pt fun i => c.proj (ε i))
• CategoryTheory.Limits.Cofan.IsColimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β) {Z : C} (h : A ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.IsColimit.desc hc f) h) = CategoryTheory.CategoryStruct.comp (f i) h
• CategoryTheory.Limits.Fan.IsLimit.fac_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : β → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β) {Z : C} (h : F i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fan.IsLimit.lift hc f) (CategoryTheory.CategoryStruct.comp (c.proj i) h) = CategoryTheory.CategoryStruct.comp (f i) h
• CategoryTheory.Limits.Cofan.isColimitMapCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {ι : Type u_1} (X : ι → C) (c : CategoryTheory.Limits.Cofan X) : CategoryTheory.Limits.IsColimit (F.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (F.obj c.pt) fun i => F.map (c.inj i))
• CategoryTheory.Limits.Fan.isLimitMapConeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {ι : Type u_1} (X : ι → C) (c : CategoryTheory.Limits.Fan X) : CategoryTheory.Limits.IsLimit (F.mapCone c) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fan.mk (F.obj c.pt) fun i => F.map (c.proj i))
• CategoryTheory.Limits.Pi.constCompPiIsoConst 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) : (CategoryTheory.Functor.pi fun i => (CategoryTheory.Functor.const (I i)).obj (X i)).comp (CategoryTheory.Limits.Pi.functor α) ≅ (CategoryTheory.Functor.const ((i : α) → I i)).obj (∏ᶜ X)
• CategoryTheory.Limits.Sigma.constCompSigmaIsoConst 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproductsOfShape α C] {I : α → Type u_1} [(i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) : (CategoryTheory.Functor.pi fun i => (CategoryTheory.Functor.const (I i)).obj (X i)).comp (CategoryTheory.Limits.Sigma.functor α) ≅ (CategoryTheory.Functor.const ((i : α) → I i)).obj (∐ X)
• CategoryTheory.Limits.Cofan.IsColimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : I → C} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f g : c.pt ⟶ A) (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp (c.inj i) f = CategoryTheory.CategoryStruct.comp (c.inj i) g) : f = g
• CategoryTheory.Limits.Fan.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : I → C} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f g : A ⟶ c.pt) (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp f (c.proj i) = CategoryTheory.CategoryStruct.comp g (c.proj i)) : f = g
• CategoryTheory.Limits.Cofan.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : c₁ ≅ c₂
• CategoryTheory.Limits.Fan.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : β → C} {c₁ c₂ : CategoryTheory.Limits.Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryTheory.CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : c₁ ≅ c₂
• CategoryTheory.Limits.Cofan.IsColimit.inj_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Cofan X} (d : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (i : β) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.inj i) (CategoryTheory.CategoryStruct.comp (hc.desc d) h) = CategoryTheory.CategoryStruct.comp (d.inj i) h
• CategoryTheory.Limits.Fan.IsLimit.lift_proj_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X : β → C} {c : CategoryTheory.Limits.Fan X} (d : CategoryTheory.Limits.Fan X) (hc : CategoryTheory.Limits.IsLimit c) (i : β) {Z : C} (h : X i ⟶ Z) : CategoryTheory.CategoryStruct.comp (hc.lift d) (CategoryTheory.CategoryStruct.comp (c.proj i) h) = CategoryTheory.CategoryStruct.comp (d.proj i) h
• CategoryTheory.Limits.Pi.isoLimit_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) = CategoryTheory.Limits.limit.π X { as := j }
• CategoryTheory.Limits.Sigma.ι_isoColimit_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasColimit X] (j : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) j) (CategoryTheory.Limits.Sigma.isoColimit X).hom = CategoryTheory.Limits.colimit.ι X { as := j }
• CategoryTheory.Limits.Pi.isoLimit_hom_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom (CategoryTheory.Limits.limit.π X { as := j }) = CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j
• CategoryTheory.Limits.Sigma.ι_isoColimit_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasColimit X] (j : α) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι X { as := j }) (CategoryTheory.Limits.Sigma.isoColimit X).inv = CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) j
• CategoryTheory.Limits.Pi.cone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Pi.cone X).π = CategoryTheory.Discrete.natTrans fun x => CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) x.as
• CategoryTheory.Limits.Sigma.cocone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] : (CategoryTheory.Limits.Sigma.cocone X).ι = CategoryTheory.Discrete.natTrans fun x => CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) x.as
• CategoryTheory.Limits.Pi.mapIso_hom_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).hom (CategoryTheory.Limits.Pi.π g b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f b) (p b).hom
• CategoryTheory.Limits.Pi.mapIso_inv_π 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).inv (CategoryTheory.Limits.Pi.π f b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) (p b).inv
• CategoryTheory.Limits.Sigma.ι_mapIso_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.Sigma.mapIso p).hom = CategoryTheory.CategoryStruct.comp (p b).hom (CategoryTheory.Limits.Sigma.ι g b)
• CategoryTheory.Limits.Sigma.ι_mapIso_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f g : β → C} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g b) (CategoryTheory.Limits.Sigma.mapIso p).inv = CategoryTheory.CategoryStruct.comp (p b).inv (CategoryTheory.Limits.Sigma.ι f b)
• CategoryTheory.Limits.Pi.isoLimit_inv_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h
• CategoryTheory.Limits.Sigma.ι_isoColimit_hom_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasColimit X] (j : α) {Z : C} (h : CategoryTheory.Limits.colimit X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.isoColimit X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι X { as := j }) h
• CategoryTheory.Limits.Pi.isoLimit_hom_π_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [CategoryTheory.Limits.HasLimit X] (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) h

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