Loogle!

Result

Found 1045 declarations mentioning CategoryTheory.Limits.Cone. Of these, only the first 200 are shown.

• CategoryTheory.Limits.Cone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : Type (max (max u₁ u₃) v₃)
• CategoryTheory.Limits.Cone.category 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Category.{v₃, max (max u₃ u₁) v₃} (CategoryTheory.Limits.Cone F)
• CategoryTheory.Limits.Cone.pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (self : CategoryTheory.Limits.Cone F) : C
• 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.Limits.ConeMorphism 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (A B : CategoryTheory.Limits.Cone F) : Type v₃
• CategoryTheory.Limits.inhabitedConeMorphism 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (A : CategoryTheory.Limits.Cone F) : Inhabited (CategoryTheory.Limits.ConeMorphism A A)
• CategoryTheory.Limits.Cone.forget 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) C
• CategoryTheory.Limits.Cones.forget 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) C
• CategoryTheory.Limits.Cocone.op 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cone F.op
• CategoryTheory.Limits.Cocone.unop 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F.op) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.Cone.op 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cocone F.op
• CategoryTheory.Limits.Cone.unop 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.coconeLeftOpOfCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cocone F.leftOp
• CategoryTheory.Limits.coconeOfConeLeftOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.coconeOfConeRightOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.coconeRightOpOfCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cocone F.rightOp
• CategoryTheory.Limits.coneLeftOpOfCocone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cone F.leftOp
• CategoryTheory.Limits.coneOfCoconeLeftOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.coneOfCoconeRightOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F.rightOp) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.coneRightOpOfCocone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cone F.rightOp
• CategoryTheory.Functor.mapCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cone (F.comp H)
• CategoryTheory.Limits.Cone.extend 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.Cone.whisker 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cone (E.comp F)
• CategoryTheory.Limits.coconeOfConeUnop 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.unop) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.coconeUnopOfCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Cocone F.unop
• CategoryTheory.Limits.coneOfCoconeUnop 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.unop) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.coneUnopOfCocone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cone F.unop
• CategoryTheory.Functor.mapConeInv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} [H.IsEquivalence] (c : CategoryTheory.Limits.Cone (F.comp H)) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.Cone.forget_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.forget F).obj t = t.pt
• CategoryTheory.Limits.Cone.eta 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c ≅ { pt := c.pt, π := c.π }
• CategoryTheory.Limits.Cone.extend_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt) : (c.extend f).pt = X
• CategoryTheory.Limits.Cones.eta 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c ≅ { pt := c.pt, π := c.π }
• CategoryTheory.Limits.ConeMorphism.hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.ConeMorphism A B) : A.pt ⟶ B.pt
• CategoryTheory.Limits.Cone.op_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c.op.pt = Opposite.op c.pt
• CategoryTheory.Limits.Cone.postcomposeEquivalence 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ≅ G) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone G
• CategoryTheory.Limits.Cones.postcomposeEquivalence 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ≅ G) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone G
• CategoryTheory.Limits.Cone.extendId 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) : s.extend (CategoryTheory.CategoryStruct.id s.pt) ≅ s
• CategoryTheory.Limits.Cones.extendId 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) : s.extend (CategoryTheory.CategoryStruct.id s.pt) ≅ s
• CategoryTheory.Limits.coconeLeftOpOfCone_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeLeftOpOfCone c).pt = Opposite.unop c.pt
• CategoryTheory.Limits.Cone.whisker_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.whisker E c).pt = c.pt
• CategoryTheory.Limits.coconeRightOpOfCone_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeRightOpOfCone c).pt = Opposite.op c.pt
• CategoryTheory.Limits.Cone.functoriality 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (F.comp G))
• CategoryTheory.Limits.Cone.whiskering 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (E.comp F))
• CategoryTheory.Limits.Cones.functoriality 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (F.comp G))
• CategoryTheory.Limits.Cones.whiskering 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone (E.comp F))
• CategoryTheory.Limits.Cone.mk 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (pt : C) (π : (CategoryTheory.Functor.const J).obj pt ⟶ F) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.coconeOfConeRightOp_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.coconeOfConeRightOp c).pt = Opposite.unop c.pt
• CategoryTheory.Limits.Cone.extendIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : s.pt ≅ X) : s ≅ s.extend f.inv
• CategoryTheory.Limits.Cone.unop_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op) : c.unop.pt = Opposite.unop c.pt
• CategoryTheory.Limits.Cones.extendIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : s.pt ≅ X) : s ≅ s.extend f.inv
• CategoryTheory.Functor.mapCone_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : (H.mapCone c).pt = H.obj c.pt
• CategoryTheory.Limits.coconeOfConeLeftOp_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp) : (CategoryTheory.Limits.coconeOfConeLeftOp c).pt = Opposite.op c.pt
• CategoryTheory.Limits.coconeOfConeUnop_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.unop) : (CategoryTheory.Limits.coconeOfConeUnop c).pt = Opposite.op c.pt
• CategoryTheory.Limits.coconeUnopOfCone_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeUnopOfCone c).pt = Opposite.unop c.pt
• CategoryTheory.Functor.mapConeInvMapCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cone F) : H.mapConeInv (H.mapCone c) ≅ c
• CategoryTheory.Limits.coconeOpEquiv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : (CategoryTheory.Limits.Cocone F)ᵒᵖ ≌ CategoryTheory.Limits.Cone F.op
• CategoryTheory.Limits.coneOpEquiv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : (CategoryTheory.Limits.Cone F)ᵒᵖ ≌ CategoryTheory.Limits.Cocone F.op
• CategoryTheory.Limits.Cone.postcompose 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone G)
• CategoryTheory.Limits.Cone.π 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (self : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.const J).obj self.pt ⟶ F
• CategoryTheory.Limits.Cones.postcompose 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G) : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone G)
• CategoryTheory.Limits.Cone.equiv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cone F ≅ (X : Cᵒᵖ) × ((CategoryTheory.Functor.const J).obj (Opposite.unop X) ⟶ F)
• CategoryTheory.Limits.Cone.extendHom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ s.pt) : s.extend f ⟶ s
• CategoryTheory.Limits.Cone.functorialityEquivalence 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (F.comp e.functor)
• CategoryTheory.Limits.Cone.whiskeringEquivalence 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (e.functor.comp F)
• CategoryTheory.Limits.Cones.extend 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ s.pt) : s.extend f ⟶ s
• CategoryTheory.Limits.Cones.functorialityEquivalence 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (F.comp e.functor)
• CategoryTheory.Limits.Cones.whiskeringEquivalence 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (e.functor.comp F)
• CategoryTheory.Limits.coconeLeftOpOfConeEquiv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} : (CategoryTheory.Limits.Cone F)ᵒᵖ ≌ CategoryTheory.Limits.Cocone F.leftOp
• CategoryTheory.Limits.coconeRightOpOfConeEquiv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} : (CategoryTheory.Limits.Cone F)ᵒᵖ ≌ CategoryTheory.Limits.Cocone F.rightOp
• CategoryTheory.Limits.coneLeftOpOfCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} : (CategoryTheory.Limits.Cocone F)ᵒᵖ ≌ CategoryTheory.Limits.Cone F.leftOp
• CategoryTheory.Limits.coneRightOpOfCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} : (CategoryTheory.Limits.Cocone F)ᵒᵖ ≌ CategoryTheory.Limits.Cone F.rightOp
• CategoryTheory.Limits.Cone.equivalenceOfReindexing 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone G
• CategoryTheory.Limits.Cone.extendHom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ s.pt) : (s.extendHom f).hom = f
• CategoryTheory.Limits.Cone.functoriality_faithful 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [G.Faithful] : (CategoryTheory.Limits.Cone.functoriality F G).Faithful
• CategoryTheory.Limits.Cone.reflects_cone_isomorphism 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] (K : CategoryTheory.Functor J C) : (CategoryTheory.Limits.Cone.functoriality K F).ReflectsIsomorphisms
• CategoryTheory.Limits.Cones.equivalenceOfReindexing 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G) : CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone G
• CategoryTheory.Limits.Cones.functoriality_faithful 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [G.Faithful] : (CategoryTheory.Limits.Cone.functoriality F G).Faithful
• CategoryTheory.Limits.Cones.reflects_cone_isomorphism 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] (K : CategoryTheory.Functor J C) : (CategoryTheory.Limits.Cone.functoriality K F).ReflectsIsomorphisms
• CategoryTheory.Limits.coconeEquivalenceOpConeOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cocone F ≌ (CategoryTheory.Limits.Cone F.op)ᵒᵖ
• CategoryTheory.Limits.coneEquivalenceOpCoconeOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.Cone F ≌ (CategoryTheory.Limits.Cocone F.op)ᵒᵖ
• CategoryTheory.Limits.Cone.instIsIsoExtendHom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {X : C} (f : X ⟶ s.pt) [CategoryTheory.IsIso f] : CategoryTheory.IsIso (s.extendHom f)
• CategoryTheory.Limits.coconeUnopOfConeEquiv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} : (CategoryTheory.Limits.Cone F)ᵒᵖ ≌ CategoryTheory.Limits.Cocone F.unop
• CategoryTheory.Limits.coneUnopOfCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} : (CategoryTheory.Limits.Cocone F)ᵒᵖ ≌ CategoryTheory.Limits.Cone F.unop
• CategoryTheory.Limits.instIsIsoHomHomCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d) : CategoryTheory.IsIso f.hom.hom
• CategoryTheory.Limits.instIsIsoHomInvCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d) : CategoryTheory.IsIso f.inv.hom
• CategoryTheory.Limits.Cone.category_id_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (B : CategoryTheory.Limits.Cone F) : (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt
• CategoryTheory.Limits.Cone.functoriality_full 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful] : (CategoryTheory.Limits.Cone.functoriality F G).Full
• CategoryTheory.Limits.Cones.functoriality_full 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful] : (CategoryTheory.Limits.Cone.functoriality F G).Full
• CategoryTheory.Limits.Cone.extensions 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : CategoryTheory.uliftYoneda.{u₁, v₃, u₃}.obj c.pt ⟶ F.cones
• CategoryTheory.Functor.mapConeMapConeInv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cone (F.comp H)) : H.mapCone (H.mapConeInv c) ≅ c
• CategoryTheory.Limits.Cone.cone_iso_of_hom_iso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {K : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone K} (f : c ⟶ d) [i : CategoryTheory.IsIso f.hom] : CategoryTheory.IsIso f
• CategoryTheory.Limits.Cones.cone_iso_of_hom_iso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {K : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone K} (f : c ⟶ d) [i : CategoryTheory.IsIso f.hom] : CategoryTheory.IsIso f
• CategoryTheory.Limits.Cone.postcompose_obj_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.postcompose α).obj c).pt = c.pt
• CategoryTheory.Limits.Cone.extendComp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : s.extend (CategoryTheory.CategoryStruct.comp f g) ≅ (s.extend g).extend f
• CategoryTheory.Limits.Cones.extendComp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : s.extend (CategoryTheory.CategoryStruct.comp f g) ≅ (s.extend g).extend f
• CategoryTheory.Limits.Cone.postcomposeId 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.id F) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)
• CategoryTheory.Limits.Cones.postcomposeId 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.id F) ≅ CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)
• CategoryTheory.Limits.Cone.whiskering_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.whiskering E).obj c = CategoryTheory.Limits.Cone.whisker E c
• CategoryTheory.Limits.Cone.functoriality_obj_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.functoriality F G).obj A).pt = G.obj A.pt
• CategoryTheory.Limits.Cone.forget_map 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) {X✝ Y✝ : CategoryTheory.Limits.Cone F} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.Cone.forget F).map f = f.hom
• CategoryTheory.Limits.Cone.postcomposeEquivalence_functor 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ≅ G) : (CategoryTheory.Limits.Cone.postcomposeEquivalence α).functor = CategoryTheory.Limits.Cone.postcompose α.hom
• CategoryTheory.Limits.Cone.postcomposeEquivalence_inverse 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ≅ G) : (CategoryTheory.Limits.Cone.postcomposeEquivalence α).inverse = CategoryTheory.Limits.Cone.postcompose α.inv
• CategoryTheory.Functor.mapConeMapCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {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 J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone F) : H'.mapCone (H.mapCone c) ≅ (H.comp H').mapCone c
• CategoryTheory.Limits.Cone.extendIso_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : s.pt ≅ X) : (s.extendIso f).hom.hom = f.hom
• CategoryTheory.Limits.Cone.extendIso_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X : C} (f : s.pt ≅ X) : (s.extendIso f).inv.hom = f.inv
• CategoryTheory.Functor.mapConeWhisker 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cone F} : H.mapCone (CategoryTheory.Limits.Cone.whisker E c) ≅ CategoryTheory.Limits.Cone.whisker E (H.mapCone c)
• CategoryTheory.Functor.mapCoconeOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cocone F) : (G.mapCocone t).op ≅ G.op.mapCone t.op
• CategoryTheory.Functor.mapConeOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F) : (G.mapCone t).op ≅ G.op.mapCocone t.op
• CategoryTheory.Limits.Cone.eta_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c.eta.hom.hom = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Limits.Cone.eta_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c.eta.inv.hom = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Functor.mapConeMorphism 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (f : c ⟶ c') : H.mapCone c ⟶ H.mapCone c'
• CategoryTheory.Limits.Cone.category_comp_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {X✝ Y✝ Z✝ : CategoryTheory.Limits.Cone F} (f : CategoryTheory.Limits.ConeMorphism X✝ Y✝) (g : CategoryTheory.Limits.ConeMorphism Y✝ Z✝) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
• CategoryTheory.Limits.Cone.functorialityEquivalence_functor 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D) : (CategoryTheory.Limits.Cone.functorialityEquivalence F e).functor = CategoryTheory.Limits.Cone.functoriality F e.functor
• CategoryTheory.Limits.Cone.whiskeringEquivalence_functor 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cone.whiskeringEquivalence e).functor = CategoryTheory.Limits.Cone.whiskering e.functor
• CategoryTheory.Limits.ConeMorphism.hom_inv_id 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d) : CategoryTheory.CategoryStruct.comp f.hom.hom f.inv.hom = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Limits.ConeMorphism.inv_hom_id 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d) : CategoryTheory.CategoryStruct.comp f.inv.hom f.hom.hom = CategoryTheory.CategoryStruct.id d.pt
• CategoryTheory.Limits.ConeMorphism.ext 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (f g : c ⟶ c') (w : f.hom = g.hom) : f = g
• CategoryTheory.Limits.ConeMorphism.ext_iff 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} {f g : c ⟶ c'} : f = g ↔ f.hom = g.hom
• CategoryTheory.Limits.Cone.extendId_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) : s.extendId.hom.hom = CategoryTheory.CategoryStruct.id s.pt
• CategoryTheory.Limits.Cone.extendId_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) : s.extendId.inv.hom = CategoryTheory.CategoryStruct.id s.pt
• CategoryTheory.Limits.Cone.whisker_π 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.whisker E c).π = E.whiskerLeft c.π
• CategoryTheory.Limits.ConeMorphism.hom_inv_id_assoc 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d) {Z : C} (h : c.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp f.hom.hom (CategoryTheory.CategoryStruct.comp f.inv.hom h) = h
• CategoryTheory.Limits.ConeMorphism.inv_hom_id_assoc 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d) {Z : C} (h : d.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp f.inv.hom (CategoryTheory.CategoryStruct.comp f.hom.hom h) = h
• CategoryTheory.Limits.Cone.op_ι 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) : c.op.ι = CategoryTheory.NatTrans.op c.π
• CategoryTheory.Limits.Cone.w 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {j j' : J} (f : j ⟶ j') : CategoryTheory.CategoryStruct.comp (c.π.app j) (F.map f) = c.π.app j'
• CategoryTheory.Limits.Cone.unop_ι 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op) : c.unop.ι = CategoryTheory.NatTrans.removeOp c.π
• CategoryTheory.Limits.coconeOpEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : (CategoryTheory.Limits.Cocone F)ᵒᵖ) : CategoryTheory.Limits.coconeOpEquiv.functor.obj c = (Opposite.unop c).op
• CategoryTheory.Limits.coconeOpEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F.op) : CategoryTheory.Limits.coconeOpEquiv.inverse.obj c = Opposite.op c.unop
• CategoryTheory.Limits.coneOpEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : (CategoryTheory.Limits.Cone F)ᵒᵖ) : CategoryTheory.Limits.coneOpEquiv.functor.obj c = (Opposite.unop c).op
• CategoryTheory.Limits.coneOpEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F.op) : CategoryTheory.Limits.coneOpEquiv.inverse.obj c = Opposite.op c.unop
• CategoryTheory.Limits.ConeMorphism.w 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.ConeMorphism A B) (j : J) : CategoryTheory.CategoryStruct.comp self.hom (B.π.app j) = A.π.app j
• CategoryTheory.Limits.Cone.whiskering_map_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (E : CategoryTheory.Functor K J) {X✝ Y✝ : CategoryTheory.Limits.Cone F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.Cone.whiskering E).map f).hom = f.hom
• CategoryTheory.Limits.coconeLeftOpOfConeEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : (CategoryTheory.Limits.Cone F)ᵒᵖ) : CategoryTheory.Limits.coconeLeftOpOfConeEquiv.functor.obj c = CategoryTheory.Limits.coconeLeftOpOfCone (Opposite.unop c)
• CategoryTheory.Limits.coconeLeftOpOfConeEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp) : CategoryTheory.Limits.coconeLeftOpOfConeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coneOfCoconeLeftOp c)
• CategoryTheory.Limits.coconeRightOpOfConeEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : (CategoryTheory.Limits.Cone F)ᵒᵖ) : CategoryTheory.Limits.coconeRightOpOfConeEquiv.functor.obj c = CategoryTheory.Limits.coconeRightOpOfCone (Opposite.unop c)
• CategoryTheory.Limits.coconeRightOpOfConeEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F.rightOp) : CategoryTheory.Limits.coconeRightOpOfConeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coneOfCoconeRightOp c)
• CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : (CategoryTheory.Limits.Cocone F)ᵒᵖ) : CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.functor.obj c = CategoryTheory.Limits.coneLeftOpOfCocone (Opposite.unop c)
• CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp) : CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coconeOfConeLeftOp c)
• CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : (CategoryTheory.Limits.Cocone F)ᵒᵖ) : CategoryTheory.Limits.coneRightOpOfCoconeEquiv.functor.obj c = CategoryTheory.Limits.coneRightOpOfCocone (Opposite.unop c)
• CategoryTheory.Limits.coneRightOpOfCoconeEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp) : CategoryTheory.Limits.coneRightOpOfCoconeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coconeOfConeRightOp c)
• CategoryTheory.Limits.coconeRightOpOfCone_ι 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeRightOpOfCone c).ι = CategoryTheory.NatTrans.rightOp c.π
• CategoryTheory.Limits.ConeMorphism.mk 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} (hom : A.pt ⟶ B.pt) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π.app j) = A.π.app j := by cat_disch) : CategoryTheory.Limits.ConeMorphism A B
• CategoryTheory.Limits.Cone.extend_π 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt) : (c.extend f).π = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f) c.π
• CategoryTheory.Functor.mapCone_π_app 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (j : J) : (H.mapCone c).π.app j = H.map (c.π.app j)
• CategoryTheory.Limits.Cone.postcompose_obj_π 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.Limits.Cone.postcompose α).obj c).π = CategoryTheory.CategoryStruct.comp c.π α
• CategoryTheory.Limits.coconeOfConeRightOp_ι 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp) : (CategoryTheory.Limits.coconeOfConeRightOp c).ι = CategoryTheory.NatTrans.removeRightOp c.π
• CategoryTheory.Limits.coconeUnopOfConeEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : (CategoryTheory.Limits.Cone F)ᵒᵖ) : CategoryTheory.Limits.coconeUnopOfConeEquiv.functor.obj c = CategoryTheory.Limits.coconeUnopOfCone (Opposite.unop c)
• CategoryTheory.Limits.coconeUnopOfConeEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.unop) : CategoryTheory.Limits.coconeUnopOfConeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coneOfCoconeUnop c)
• CategoryTheory.Limits.coneUnopOfCoconeEquiv_functor_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : (CategoryTheory.Limits.Cocone F)ᵒᵖ) : CategoryTheory.Limits.coneUnopOfCoconeEquiv.functor.obj c = CategoryTheory.Limits.coneUnopOfCocone (Opposite.unop c)
• CategoryTheory.Limits.coneUnopOfCoconeEquiv_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.unop) : CategoryTheory.Limits.coneUnopOfCoconeEquiv.inverse.obj c = Opposite.op (CategoryTheory.Limits.coconeOfConeUnop c)
• CategoryTheory.Functor.postcomposeWhiskerLeftMapCone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.postcompose (F.whiskerLeft α.hom)).obj (H.mapCone c) ≅ H'.mapCone c
• CategoryTheory.Limits.Cone.extInv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j := by cat_disch) : c ≅ c'
• CategoryTheory.Limits.Cone.postcomposeComp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G H : CategoryTheory.Functor J C} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.comp α β) ≅ (CategoryTheory.Limits.Cone.postcompose α).comp (CategoryTheory.Limits.Cone.postcompose β)
• CategoryTheory.Limits.Cones.postcomposeComp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G H : CategoryTheory.Functor J C} (α : F ⟶ G) (β : G ⟶ H) : CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.comp α β) ≅ (CategoryTheory.Limits.Cone.postcompose α).comp (CategoryTheory.Limits.Cone.postcompose β)
• CategoryTheory.Limits.coconeUnopOfCone_ι 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.coconeUnopOfCone c).ι = CategoryTheory.NatTrans.unop c.π
• CategoryTheory.Limits.Cone.w_assoc 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {j j' : J} (f : j ⟶ j') {Z : C} (h : F.obj j' ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.π.app j) (CategoryTheory.CategoryStruct.comp (F.map f) h) = CategoryTheory.CategoryStruct.comp (c.π.app j') h
• CategoryTheory.Limits.ConeMorphism.w_assoc 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.ConeMorphism A B) (j : J) {Z : C} (h : F.obj j ⟶ Z) : CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp (B.π.app j) h) = CategoryTheory.CategoryStruct.comp (A.π.app j) h
• CategoryTheory.Limits.coconeOfConeUnop_ι 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.unop) : (CategoryTheory.Limits.coconeOfConeUnop c).ι = CategoryTheory.NatTrans.removeUnop c.π
• CategoryTheory.Limits.Cone.extendComp_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : (s.extendComp f g).hom.hom = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.Cone.extendComp_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt) : (s.extendComp f g).inv.hom = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.Cone.ext 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j) := by cat_disch) : c ≅ c'
• CategoryTheory.Limits.Cones.ext 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j) := by cat_disch) : c ≅ c'
• CategoryTheory.Functor.mapConePostcompose 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cone F} : H.mapCone ((CategoryTheory.Limits.Cone.postcompose α).obj c) ≅ (CategoryTheory.Limits.Cone.postcompose (CategoryTheory.Functor.whiskerRight α H)).obj (H.mapCone c)
• CategoryTheory.Limits.Cone.functoriality_obj_π_app 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (G : CategoryTheory.Functor C D) (A : CategoryTheory.Limits.Cone F) (j : J) : ((CategoryTheory.Limits.Cone.functoriality F G).obj A).π.app j = G.map (A.π.app j)
• CategoryTheory.Limits.Cone.equivalenceOfReindexing_functor 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G) : (CategoryTheory.Limits.Cone.equivalenceOfReindexing e α).functor = (CategoryTheory.Limits.Cone.whiskering e.functor).comp (CategoryTheory.Limits.Cone.postcompose α.hom)
• CategoryTheory.Functor.functorialityCompPostcompose 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H H' : CategoryTheory.Functor C D} (α : H ≅ H') : (CategoryTheory.Limits.Cone.functoriality F H).comp (CategoryTheory.Limits.Cone.postcompose (F.whiskerLeft α.hom)) ≅ CategoryTheory.Limits.Cone.functoriality F H'
• CategoryTheory.Limits.Cone.extInv_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j := by cat_disch) : (CategoryTheory.Limits.Cone.extInv φ w).hom.hom = φ.hom
• CategoryTheory.Limits.Cone.extInv_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j := by cat_disch) : (CategoryTheory.Limits.Cone.extInv φ w).inv.hom = φ.inv
• CategoryTheory.Limits.Cone.functorialityCompFunctoriality 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {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 J C) (G : CategoryTheory.Functor C D) (H : CategoryTheory.Functor D E) : (CategoryTheory.Limits.Cone.functoriality F G).comp (CategoryTheory.Limits.Cone.functoriality (F.comp G) H) ≅ CategoryTheory.Limits.Cone.functoriality F (G.comp H)
• CategoryTheory.Limits.Cones.functorialityCompFunctoriality 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {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 J C) (G : CategoryTheory.Functor C D) (H : CategoryTheory.Functor D E) : (CategoryTheory.Limits.Cone.functoriality F G).comp (CategoryTheory.Limits.Cone.functoriality (F.comp G) H) ≅ CategoryTheory.Limits.Cone.functoriality F (G.comp H)
• CategoryTheory.Limits.coconeLeftOpOfCone_ι_app 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F) (X : Jᵒᵖ) : (CategoryTheory.Limits.coconeLeftOpOfCone c).ι.app X = (c.π.app (Opposite.unop X)).unop
• CategoryTheory.Limits.Cone.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j) := by cat_disch) : (CategoryTheory.Limits.Cone.ext φ w).hom.hom = φ.hom
• CategoryTheory.Limits.Cone.ext_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt) (w : ∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j) := by cat_disch) : (CategoryTheory.Limits.Cone.ext φ w).inv.hom = φ.inv
• CategoryTheory.Limits.Cone.postcompose_map_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F G : CategoryTheory.Functor J C} (α : F ⟶ G) {X✝ Y✝ : CategoryTheory.Limits.Cone F} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Limits.Cone.postcompose α).map f).hom = f.hom
• CategoryTheory.Functor.mapConePostcomposeEquivalenceFunctor 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cone F} : H.mapCone ((CategoryTheory.Limits.Cone.postcomposeEquivalence α).functor.obj c) ≅ (CategoryTheory.Limits.Cone.postcomposeEquivalence (CategoryTheory.Functor.isoWhiskerRight α H)).functor.obj (H.mapCone c)
• CategoryTheory.Limits.coconeOpEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.coconeOpEquiv.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ)
• CategoryTheory.Limits.coneOpEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} : CategoryTheory.Limits.coneOpEquiv.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ)
• CategoryTheory.Limits.ConeMorphism.map_w 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (f : c ⟶ c') (G : CategoryTheory.Functor C D) (j : J) : CategoryTheory.CategoryStruct.comp (G.map f.hom) (G.map (c'.π.app j)) = G.map (c.π.app j)
• CategoryTheory.Limits.coconeOfConeLeftOp_ι_app 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cone F.leftOp) (X : J) : (CategoryTheory.Limits.coconeOfConeLeftOp c).ι.app X = (c.π.app (Opposite.op X)).op
• CategoryTheory.Functor.mapConeMapCone_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {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 J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.mapConeMapCone c).hom.hom = CategoryTheory.CategoryStruct.id (H'.obj (H.obj c.pt))
• CategoryTheory.Functor.mapConeMapCone_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {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 J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.mapConeMapCone c).inv.hom = CategoryTheory.CategoryStruct.id (H'.obj (H.obj c.pt))
• CategoryTheory.Functor.mapConeWhisker_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cone F} : H.mapConeWhisker.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
• CategoryTheory.Functor.mapConeWhisker_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cone F} : H.mapConeWhisker.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
• CategoryTheory.Limits.Cone.whiskeringEquivalence_inverse 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J) : (CategoryTheory.Limits.Cone.whiskeringEquivalence e).inverse = (CategoryTheory.Limits.Cone.whiskering e.inverse).comp (CategoryTheory.Limits.Cone.postcompose (e.invFunIdAssoc F).hom)
• CategoryTheory.Limits.coconeOpEquiv_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {Y✝ X✝ : (CategoryTheory.Limits.Cocone F)ᵒᵖ} (f : Y✝ ⟶ X✝) : (CategoryTheory.Limits.coconeOpEquiv.functor.map f).hom = f.unop.hom.op
• CategoryTheory.Limits.coneOpEquiv_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {X✝ Y✝ : (CategoryTheory.Limits.Cone F)ᵒᵖ} (f : X✝ ⟶ Y✝) : (CategoryTheory.Limits.coneOpEquiv.functor.map f).hom = f.unop.hom.op
• CategoryTheory.Limits.ConeMorphism.map_w_assoc 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (f : c ⟶ c') (G : CategoryTheory.Functor C D) (j : J) {Z : D} (h : G.obj (F.obj j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (G.map f.hom) (CategoryTheory.CategoryStruct.comp (G.map (c'.π.app j)) h) = CategoryTheory.CategoryStruct.comp (G.map (c.π.app j)) h
• CategoryTheory.Functor.mapCoconeOp_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.mapCoconeOp G t).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
• CategoryTheory.Functor.mapCoconeOp_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.mapCoconeOp G t).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
• CategoryTheory.Functor.mapConeOp_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.mapConeOp G t).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
• CategoryTheory.Functor.mapConeOp_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.mapConeOp G t).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
• CategoryTheory.Limits.Cone.w_apply 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {j j' : J} (f : j ⟶ j') {F✝ : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F✝ X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory C F✝] (x : carrier c.pt) : (CategoryTheory.ConcreteCategory.hom (F.map f)) ((CategoryTheory.ConcreteCategory.hom (c.π.app j)) x) = (CategoryTheory.ConcreteCategory.hom (c.π.app j')) x
• CategoryTheory.Limits.Cone.equiv_hom_hom_apply_fst 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Cone.equiv F).hom) c).fst = Opposite.op c.pt
• CategoryTheory.Limits.Cone.extensions_app 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (x✝ : Cᵒᵖ) : c.extensions.app x✝ = TypeCat.ofHom fun f => CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f.down) c.π
• CategoryTheory.Limits.Cone.postcomposeId_hom_app_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (X : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.postcomposeId.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.Cone.postcomposeId_inv_app_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (X : CategoryTheory.Limits.Cone F) : (CategoryTheory.Limits.Cone.postcomposeId.inv.app X).hom = CategoryTheory.CategoryStruct.id X.pt
• CategoryTheory.Limits.coconeLeftOpOfConeEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} : CategoryTheory.Limits.coconeLeftOpOfConeEquiv.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ)
• CategoryTheory.Limits.coconeRightOpOfConeEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} : CategoryTheory.Limits.coconeRightOpOfConeEquiv.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)ᵒᵖ)
• CategoryTheory.Limits.coneLeftOpOfCoconeEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J Cᵒᵖ} : CategoryTheory.Limits.coneLeftOpOfCoconeEquiv.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ)
• CategoryTheory.Limits.coneRightOpOfCoconeEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor Jᵒᵖ C} : CategoryTheory.Limits.coneRightOpOfCoconeEquiv.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone F)ᵒᵖ)

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