Loogle!

Result

Found 94 declarations mentioning CategoryTheory.Limits.BinaryCofan.

• CategoryTheory.Limits.BinaryCofan 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] (X Y : C) : Type (max u v)
• CategoryTheory.Limits.BinaryCofan.op 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) : CategoryTheory.Limits.BinaryFan (Opposite.op X) (Opposite.op Y)
• CategoryTheory.Limits.BinaryCofan.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan (Opposite.op X) (Opposite.op Y)) : CategoryTheory.Limits.BinaryFan X Y
• CategoryTheory.Limits.BinaryFan.op 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryFan X Y) : CategoryTheory.Limits.BinaryCofan (Opposite.op X) (Opposite.op Y)
• CategoryTheory.Limits.BinaryFan.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryFan (Opposite.op X) (Opposite.op Y)) : CategoryTheory.Limits.BinaryCofan X Y
• CategoryTheory.Limits.BinaryCofan.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (ι₁ : X ⟶ P) (ι₂ : Y ⟶ P) : CategoryTheory.Limits.BinaryCofan X Y
• CategoryTheory.Limits.BinaryCofan.map 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D) {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : CategoryTheory.Limits.BinaryCofan (F.obj X) (F.obj Y)
• CategoryTheory.Limits.BinaryCofan.IsColimit.op 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsLimit c.op
• CategoryTheory.Limits.BinaryCofan.IsColimit.unop 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan (Opposite.op X) (Opposite.op Y)} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsLimit c.unop
• CategoryTheory.Limits.BinaryCofan.IsColimit.desc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : s.pt ⟶ W
• CategoryTheory.Limits.BinaryCofan.inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.left }
• CategoryTheory.Limits.BinaryCofan.inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj { as := CategoryTheory.Limits.WalkingPair.right }
• CategoryTheory.Limits.BinaryFan.op_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : P ⟶ X) (π₂ : P ⟶ Y) : (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).op = CategoryTheory.Limits.BinaryCofan.mk π₁.op π₂.op
• CategoryTheory.Limits.BinaryCofan.isColimitMapConeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y} : CategoryTheory.Limits.IsColimit (F.mapCocone s) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.map F s)
• CategoryTheory.Limits.isoBinaryCofanMk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) : c ≅ CategoryTheory.Limits.BinaryCofan.mk c.inl c.inr
• CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsInitial Y) (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inl
• CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Limits.IsInitial X) (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ CategoryTheory.IsIso c.inr
• CategoryTheory.Limits.BinaryFan.unop_mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y P : C} (π₁ : Opposite.op P ⟶ Opposite.op X) (π₂ : Opposite.op P ⟶ Opposite.op Y) : (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).unop = CategoryTheory.Limits.BinaryCofan.mk π₁.unop π₂.unop
• CategoryTheory.Limits.BinaryCofan.ι_app_left 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : s.ι.app { as := CategoryTheory.Limits.WalkingPair.left } = s.inl
• CategoryTheory.Limits.BinaryCofan.ι_app_right 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : s.ι.app { as := CategoryTheory.Limits.WalkingPair.right } = s.inr
• CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : CategoryTheory.CategoryStruct.comp s.inl (CategoryTheory.Limits.BinaryCofan.IsColimit.desc h f g) = f
• CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : CategoryTheory.CategoryStruct.comp s.inr (CategoryTheory.Limits.BinaryCofan.IsColimit.desc h f g) = g
• CategoryTheory.Limits.BinaryCofan.isColimitFlip 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk c.inr c.inl)
• CategoryTheory.Limits.BinaryCofan.isColimitCompLeftIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y X' : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (f : X' ⟶ X) [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.comp f c.inl) c.inr)
• CategoryTheory.Limits.BinaryCofan.isColimitCompRightIso 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Y' : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (f : Y' ⟶ Y) [CategoryTheory.IsIso f] (h : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk c.inl (CategoryTheory.CategoryStruct.comp f c.inr))
• CategoryTheory.Limits.BinaryCofan.map_inl 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.BinaryCofan.map F s).inl = F.map s.inl
• CategoryTheory.Limits.BinaryCofan.map_inr 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.BinaryCofan.map F s).inr = F.map s.inr
• CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp s.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.IsColimit.desc h f g) h✝) = CategoryTheory.CategoryStruct.comp f h✝
• CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) {Z : C} (h✝ : W ⟶ Z) : CategoryTheory.CategoryStruct.comp s.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.IsColimit.desc h f g) h✝) = CategoryTheory.CategoryStruct.comp g h✝
• CategoryTheory.Limits.BinaryCofan.IsColimit.desc' 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : { l // CategoryTheory.CategoryStruct.comp s.inl l = f ∧ CategoryTheory.CategoryStruct.comp s.inr l = g }
• CategoryTheory.Limits.BinaryCofan.isColimitMk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y W : C} {inl : X ⟶ W} {inr : Y ⟶ W} (desc : (s : CategoryTheory.Limits.BinaryCofan X Y) → W ⟶ s.pt) (fac_left : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inl (desc s) = s.inl) (fac_right : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inr (desc s) = s.inr) (uniq : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y) (m : W ⟶ s.pt), CategoryTheory.CategoryStruct.comp inl m = s.inl → CategoryTheory.CategoryStruct.comp inr m = s.inr → m = desc s) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr)
• CategoryTheory.Limits.BinaryCofan.IsColimit.desc'_coe 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) (f : X ⟶ W) (g : Y ⟶ W) : ↑(CategoryTheory.Limits.BinaryCofan.IsColimit.desc' h f g) = h.desc (CategoryTheory.Limits.BinaryCofan.mk f g)
• CategoryTheory.Limits.BinaryCofan.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : CategoryTheory.CategoryStruct.comp c.inl e.hom = c'.inl) (h₂ : CategoryTheory.CategoryStruct.comp c.inr e.hom = c'.inr) : c ≅ c'
• CategoryTheory.Limits.BinaryCofan.IsColimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit s) {f g : s.pt ⟶ W} (h₁ : CategoryTheory.CategoryStruct.comp s.inl f = CategoryTheory.CategoryStruct.comp s.inl g) (h₂ : CategoryTheory.CategoryStruct.comp s.inr f = CategoryTheory.CategoryStruct.comp s.inr g) : f = g
• CategoryTheory.Limits.BinaryCofan.ext_hom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A B : C} {c c' : CategoryTheory.Limits.BinaryCofan A B} (e : c.pt ≅ c'.pt) (h₁ : CategoryTheory.CategoryStruct.comp c.inl e.hom = c'.inl) (h₂ : CategoryTheory.CategoryStruct.comp c.inr e.hom = c'.inr) : (CategoryTheory.Limits.BinaryCofan.ext e h₁ h₂).hom.hom = e.hom
• CategoryTheory.Limits.BinaryCofan.IsColimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) (desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)) (hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), CategoryTheory.CategoryStruct.comp s.inl (desc f g) = f) (hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), CategoryTheory.CategoryStruct.comp s.inr (desc f g) = g) (uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), CategoryTheory.CategoryStruct.comp s.inl m = f → CategoryTheory.CategoryStruct.comp s.inr m = g → m = desc f g) : CategoryTheory.Limits.IsColimit s
• CategoryTheory.IsPushout.of_isColimit_binaryCofan_of_isInitial 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) {I : C} (hI : CategoryTheory.Limits.IsInitial I) : CategoryTheory.IsPushout (hI.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) (hI.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) c.inr c.inl
• CategoryTheory.IsPushout.of_is_coproduct 📋 Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit c) (t : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.IsPushout (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
• CommRingCat.coproductCocone 📋 Mathlib.Algebra.Category.Ring.Constructions
  (A B : CommRingCat) : CategoryTheory.Limits.BinaryCofan A B
• CommRingCat.coproductCoconeIsColimit_desc 📋 Mathlib.Algebra.Category.Ring.Constructions
  (A B : CommRingCat) (s : CategoryTheory.Limits.BinaryCofan A B) : (A.coproductCoconeIsColimit B).desc s = CommRingCat.ofHom (Algebra.TensorProduct.lift (CommRingCat.Hom.hom s.inl).toIntAlgHom (CommRingCat.Hom.hom s.inr).toIntAlgHom ⋯).toRingHom
• CategoryTheory.extendCofan 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) : CategoryTheory.Limits.Cofan f
• CategoryTheory.extendCofan_pt 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) : (CategoryTheory.extendCofan c₁ c₂).pt = c₂.pt
• CategoryTheory.extendCofanIsColimit 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : CategoryTheory.Limits.IsColimit c₁) (t₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.IsColimit (CategoryTheory.extendCofan c₁ c₂)
• CategoryTheory.extendCofan_ι_app 📋 Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} {f : Fin (n + 1) → C} (c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) : (CategoryTheory.extendCofan c₁ c₂).ι.app X = Fin.cases c₂.inl (fun i => CategoryTheory.CategoryStruct.comp (c₁.ι.app { as := i }) c₂.inr) X.as
• CommAlgCat.binaryCofan 📋 Mathlib.Algebra.Category.CommAlgCat.Monoidal
  {R : Type u} [CommRing R] (A B : CommAlgCat R) : CategoryTheory.Limits.BinaryCofan A B
• CategoryTheory.Limits.Types.binaryCoproductColimit_desc 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  (X Y : Type u) (s : CategoryTheory.Limits.BinaryCofan X Y) : (CategoryTheory.Limits.Types.binaryCoproductColimit X Y).desc s = TypeCat.ofHom (Sum.elim ⇑(CategoryTheory.ConcreteCategory.hom s.inl) ⇑(CategoryTheory.ConcreteCategory.hom s.inr))
• CategoryTheory.Limits.Types.binaryCofan_isColimit_iff 📋 Mathlib.CategoryTheory.Limits.Types.Coproducts
  {X Y : Type u} (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom c.inl) ∧ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom c.inr) ∧ IsCompl (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inl)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inr))
• CategoryTheory.ObjectProperty.prop_of_isColimit_binaryCofan 📋 Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderBinaryCoproducts] {X Y : C} {B : CategoryTheory.Limits.BinaryCofan X Y} (hB : CategoryTheory.Limits.IsColimit B) (hX : P X) (hY : P Y) : P B.pt
• TopCat.binaryCofan 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  (X Y : TopCat) : CategoryTheory.Limits.BinaryCofan X Y
• TopCat.binaryCofan_isColimit_iff 📋 Mathlib.Topology.Category.TopCat.Limits.Products
  {X Y : TopCat} (c : CategoryTheory.Limits.BinaryCofan X Y) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inl) ∧ Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inr) ∧ IsCompl (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inl)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inr))
• CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasInitial C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.IsVanKampenColimit c) : CategoryTheory.Mono c.inr
• CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasInitial C] {c : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.IsVanKampenColimit c) : CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
• CategoryTheory.isUniversalColimit_extendCofan 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : CategoryTheory.IsUniversalColimit c₁) (t₂ : CategoryTheory.IsUniversalColimit c₂) [∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback c₂.inr i] : CategoryTheory.IsUniversalColimit (CategoryTheory.extendCofan c₁ c₂)
• CategoryTheory.isVanKampenColimit_extendCofan 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : CategoryTheory.IsVanKampenColimit c₁) (t₂ : CategoryTheory.IsVanKampenColimit c₂) [∀ {Z : C} (i : Z ⟶ c₂.pt), CategoryTheory.Limits.HasPullback c₂.inr i] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.IsVanKampenColimit (CategoryTheory.extendCofan c₁ c₂)
• CategoryTheory.BinaryCofan.isVanKampen_iff 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) : CategoryTheory.IsVanKampenColimit c ↔ ∀ {X' Y' : C} (c' : CategoryTheory.Limits.BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt), CategoryTheory.CategoryStruct.comp αX c.inl = CategoryTheory.CategoryStruct.comp c'.inl f → CategoryTheory.CategoryStruct.comp αY c.inr = CategoryTheory.CategoryStruct.comp c'.inr f → (Nonempty (CategoryTheory.Limits.IsColimit c') ↔ CategoryTheory.IsPullback c'.inl αX f c.inl ∧ CategoryTheory.IsPullback c'.inr αY f c.inr)
• CategoryTheory.BinaryCofan.isVanKampen_mk 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (cofans : (X Y : C) → CategoryTheory.Limits.BinaryCofan X Y) (colimits : (X Y : C) → CategoryTheory.Limits.IsColimit (cofans X Y)) (cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.PullbackCone f g) (limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.IsLimit (cones f g)) (h₁ : ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt), CategoryTheory.CategoryStruct.comp αX c.inl = CategoryTheory.CategoryStruct.comp (cofans X' Y').inl f → CategoryTheory.CategoryStruct.comp αY c.inr = CategoryTheory.CategoryStruct.comp (cofans X' Y').inr f → CategoryTheory.IsPullback (cofans X' Y').inl αX f c.inl ∧ CategoryTheory.IsPullback (cofans X' Y').inr αY f c.inr) (h₂ : {Z : C} → (f : Z ⟶ c.pt) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)) : CategoryTheory.IsVanKampenColimit c
• CategoryTheory.Limits.MonoCoprod.binaryCofan_inl 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} {inst✝ : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Limits.MonoCoprod C] ⦃A B : C⦄ (c : CategoryTheory.Limits.BinaryCofan A B) : ∀ (x : CategoryTheory.Limits.IsColimit c), CategoryTheory.Mono c.inl
• CategoryTheory.Limits.MonoCoprod.binaryCofan_inr 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B : C} [CategoryTheory.Limits.MonoCoprod C] (c : CategoryTheory.Limits.BinaryCofan A B) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Mono c.inr
• CategoryTheory.Limits.MonoCoprod.mk 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (binaryCofan_inl : ∀ ⦃A B : C⦄ (c : CategoryTheory.Limits.BinaryCofan A B) (x : CategoryTheory.Limits.IsColimit c), CategoryTheory.Mono c.inl) : CategoryTheory.Limits.MonoCoprod C
• CategoryTheory.Limits.MonoCoprod.mk' 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (h : ∀ (A B : C), ∃ c x, CategoryTheory.Mono c.inl) : CategoryTheory.Limits.MonoCoprod C
• CategoryTheory.Limits.MonoCoprod.binaryCofanSum 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt
• CategoryTheory.Limits.MonoCoprod.mono_inl_iff 📋 Mathlib.CategoryTheory.Limits.MonoCoprod
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {A B : C} {c₁ c₂ : CategoryTheory.Limits.BinaryCofan A B} (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Mono c₁.inl ↔ CategoryTheory.Mono c₂.inl
• CategoryTheory.Mono.cofanInl_of_binaryCoproductDisjoint 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Mono c.inl
• CategoryTheory.Mono.cofanInr_of_binaryCoproductDisjoint 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Mono c.inr
• CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimitOfIsLimit 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) {s : CategoryTheory.Limits.PullbackCone c.inl c.inr} (hs : CategoryTheory.Limits.IsLimit s) : CategoryTheory.Limits.IsInitial s.pt
• CategoryTheory.Limits.BinaryCoproductDisjoint.of_binaryCofan 📋 Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Mono c.inl] [CategoryTheory.Mono c.inr] {s : CategoryTheory.Limits.PullbackCone c.inl c.inr} (hs : CategoryTheory.Limits.IsLimit s) (H : CategoryTheory.Limits.IsInitial s.pt) : CategoryTheory.Limits.BinaryCoproductDisjoint X Y
• CategoryTheory.FinitaryExtensive.van_kampen' 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryExtensive C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) : ∀ (a : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsVanKampenColimit c
• CategoryTheory.FinitaryPreExtensive.universal' 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} {inst✝ : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryPreExtensive C] {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) : ∀ (a : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsUniversalColimit c
• CategoryTheory.FinitaryExtensive.mk 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C] [hasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions C] (van_kampen' : ∀ {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (a : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsVanKampenColimit c) : CategoryTheory.FinitaryExtensive C
• CategoryTheory.FinitaryPreExtensive.mk 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] [hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C] [hasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions C] (universal' : ∀ {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (a : CategoryTheory.Limits.IsColimit c), CategoryTheory.IsUniversalColimit c) : CategoryTheory.FinitaryPreExtensive C
• CategoryTheory.finitaryExtensive_iff_of_isTerminal 📋 Mathlib.CategoryTheory.Extensive
  (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.HasPullbacksOfInclusions C] (T : C) (HT : CategoryTheory.Limits.IsTerminal T) (c₀ : CategoryTheory.Limits.BinaryCofan T T) (hc₀ : CategoryTheory.Limits.IsColimit c₀) : CategoryTheory.FinitaryExtensive C ↔ CategoryTheory.IsVanKampenColimit c₀
• CategoryTheory.FinitaryExtensive.mono_inl_of_isColimit 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.FinitaryExtensive C] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Mono c.inl
• CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.FinitaryExtensive C] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Mono c.inr
• CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan 📋 Mathlib.CategoryTheory.Extensive
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.FinitaryExtensive C] {c : CategoryTheory.Limits.BinaryCofan X Y} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.IsPullback (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (CategoryTheory.Limits.initial.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr
• CategoryTheory.IsPushout.isVanKampen_inl 📋 Mathlib.CategoryTheory.Adhesive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {W E X Z : C} (c : CategoryTheory.Limits.BinaryCofan W E) [CategoryTheory.FinitaryExtensive C] [CategoryTheory.Limits.HasPullbacks C] (hc : CategoryTheory.Limits.IsColimit c) (f : W ⟶ X) (h : X ⟶ Z) (i : c.pt ⟶ Z) (H : CategoryTheory.IsPushout f c.inl h i) : H.IsVanKampen
• CategoryTheory.is_coprod_iff_isPushout 📋 Mathlib.CategoryTheory.Adhesive.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X E Y YE : C} (c : CategoryTheory.Limits.BinaryCofan X E) (hc : CategoryTheory.Limits.IsColimit c) {f : X ⟶ Y} {iY : Y ⟶ YE} {fE : c.pt ⟶ YE} (H : CategoryTheory.CommSq f c.inl iY fE) : Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.CategoryStruct.comp c.inr fE) iY)) ↔ CategoryTheory.IsPushout f c.inl iY fE
• Preorder.semilatticeSupOfIsColimitBinaryCofan 📋 Mathlib.CategoryTheory.Limits.Preorder
  {C : Type u} [PartialOrder C] (c : (X Y : C) → CategoryTheory.Limits.BinaryCofan X Y) (h : (X Y : C) → CategoryTheory.Limits.IsColimit (c X Y)) : SemilatticeSup C
• CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} : CategoryTheory.Limits.PushoutCocone f g ≌ CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)
• CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : CategoryTheory.Limits.PushoutCocone f g} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.functor.obj c)
• CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanInverse 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.inverse.obj c)
• CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : CategoryTheory.Limits.PushoutCocone f g) : CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.functor.obj c = CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c.inl ⋯) (CategoryTheory.Under.homMk c.inr ⋯)
• CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)) : CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.inverse.obj c = CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right c.inl) (CategoryTheory.Under.Hom.right c.inr) ⋯
• CategoryTheory.Limits.IsColimit.pushoutCoconeEquivBinaryCofanFunctor_desc_right 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c : CategoryTheory.Limits.PushoutCocone f g} (hc : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)) : (hc.pushoutCoconeEquivBinaryCofanFunctor.desc s).right = hc.desc (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right s.inl) (CategoryTheory.Under.Hom.right s.inr) ⋯)
• CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_inverse_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c₁ c₂ : CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)} (a : c₁ ⟶ c₂) : (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.inverse.map a).hom = CategoryTheory.Under.Hom.right a.hom
• CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_functor_map_hom 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {c₁ c₂ : CategoryTheory.Limits.PushoutCocone f g} (a : c₁ ⟶ c₂) : (CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.functor.map a).hom = CategoryTheory.Under.homMk a.hom ⋯
• CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_unitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} : CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.unitIso = CategoryTheory.NatIso.ofComponents (fun c => c.eta) ⋯
• CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan_counitIso 📋 Mathlib.CategoryTheory.Limits.Constructions.Over.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} : CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan.counitIso = CategoryTheory.NatIso.ofComponents (fun X_1 => CategoryTheory.Limits.BinaryCofan.ext (CategoryTheory.Under.isoMk (CategoryTheory.Iso.refl (({ obj := fun c => CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Under.Hom.right c.inl) (CategoryTheory.Under.Hom.right c.inr) ⋯, map := fun {c₁ c₂} a => { hom := CategoryTheory.Under.Hom.right a.hom, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun c => CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Under.homMk c.inl ⋯) (CategoryTheory.Under.homMk c.inr ⋯), map := fun {c₁ c₂} a => { hom := CategoryTheory.Under.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯, map_comp := ⋯ }).obj X_1).pt.right) ⋯) ⋯ ⋯) ⋯
• CategoryTheory.Limits.binaryCofanZeroLeft 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.BinaryCofan 0 X
• CategoryTheory.Limits.binaryCofanZeroRight 📋 Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.Limits.BinaryCofan X 0
• CategoryTheory.Limits.Cofan.combPairHoms 📋 Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {ι₁ : Type u_1} {ι₂ : Type u_2} {f₁ : ι₁ → C} {f₂ : ι₂ → C} (c₁ : CategoryTheory.Limits.Cofan f₁) (c₂ : CategoryTheory.Limits.Cofan f₂) (bc : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt) (i : ι₁ ⊕ ι₂) : Sum.elim f₁ f₂ i ⟶ bc.pt
• CategoryTheory.Limits.Cofan.combPairIsColimit 📋 Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts
  {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {ι₁ : Type u_1} {ι₂ : Type u_2} {f₁ : ι₁ → C} {f₂ : ι₂ → C} {c₁ : CategoryTheory.Limits.Cofan f₁} {c₂ : CategoryTheory.Limits.Cofan f₂} {bc : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt} (h₁ : CategoryTheory.Limits.IsColimit c₁) (h₂ : CategoryTheory.Limits.IsColimit c₂) (h : CategoryTheory.Limits.IsColimit bc) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk bc.pt (c₁.combPairHoms c₂ bc))
• CategoryTheory.FunctorToTypes.binaryCoproductCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) : CategoryTheory.Limits.BinaryCofan F G
• CategoryTheory.FunctorToTypes.binaryCoproductColimit_desc 📋 Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
  {C : Type u} [CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (s : CategoryTheory.Limits.BinaryCofan F G) : (CategoryTheory.FunctorToTypes.binaryCoproductColimit F G).desc s = CategoryTheory.FunctorToTypes.coprod.desc s.inl s.inr
• CompHausLike.coproductCocone 📋 Mathlib.Topology.Category.CompHausLike.Cartesian
  {P : TopCat → Prop} (X Y : CompHausLike P) [CompHausLike.HasProp P (↑X.toTop ⊕ ↑Y.toTop)] : CategoryTheory.Limits.BinaryCofan X Y

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