Loogle!

Result

Found 97 declarations mentioning CategoryTheory.Limits.WalkingParallelFamily.

• CategoryTheory.Limits.WalkingParallelFamily 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (J : Type w) : Type w
• CategoryTheory.Limits.WalkingParallelFamily.one 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} : CategoryTheory.Limits.WalkingParallelFamily J
• CategoryTheory.Limits.WalkingParallelFamily.zero 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} : CategoryTheory.Limits.WalkingParallelFamily J
• CategoryTheory.Limits.instDecidableEqWalkingParallelFamily 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} : DecidableEq (CategoryTheory.Limits.WalkingParallelFamily J)
• CategoryTheory.Limits.instInhabitedWalkingParallelFamily 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {a✝ : Type u_1} : Inhabited (CategoryTheory.Limits.WalkingParallelFamily a✝)
• CategoryTheory.Limits.WalkingParallelFamily.category 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} : CategoryTheory.SmallCategory (CategoryTheory.Limits.WalkingParallelFamily J)
• CategoryTheory.Limits.WalkingParallelFamily.Hom 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (J : Type w) : CategoryTheory.Limits.WalkingParallelFamily J → CategoryTheory.Limits.WalkingParallelFamily J → Type w
• CategoryTheory.Limits.WalkingParallelFamily.Hom.id 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} (X : CategoryTheory.Limits.WalkingParallelFamily J) : CategoryTheory.Limits.WalkingParallelFamily.Hom J X X
• CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool) ≌ CategoryTheory.Limits.WalkingParallelPair
• CategoryTheory.Limits.WalkingParallelFamily.arrowEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (J : Type w) : CategoryTheory.Arrow (CategoryTheory.Limits.WalkingParallelFamily J) ≃ Option (Option J)
• CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J✝ : Type u_1} {a✝ a✝¹ : CategoryTheory.Limits.WalkingParallelFamily J✝} [DecidableEq J✝] : DecidableEq (CategoryTheory.Limits.WalkingParallelFamily.Hom J✝ a✝ a✝¹)
• CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {J' : Type w'} (e : J ≃ J') : CategoryTheory.Limits.WalkingParallelFamily J ≌ CategoryTheory.Limits.WalkingParallelFamily J'
• CategoryTheory.Limits.WalkingParallelFamily.Hom.comp 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {X Y Z : CategoryTheory.Limits.WalkingParallelFamily J} : CategoryTheory.Limits.WalkingParallelFamily.Hom J X Y → CategoryTheory.Limits.WalkingParallelFamily.Hom J Y Z → CategoryTheory.Limits.WalkingParallelFamily.Hom J X Z
• CategoryTheory.Limits.WalkingParallelFamily.hom_id 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} (X : CategoryTheory.Limits.WalkingParallelFamily J) : CategoryTheory.Limits.WalkingParallelFamily.Hom.id X = CategoryTheory.CategoryStruct.id X
• CategoryTheory.Limits.parallelFamily 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C
• CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom.decEq 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J✝ : Type u_1} {a✝ a✝¹ : CategoryTheory.Limits.WalkingParallelFamily J✝} [DecidableEq J✝] (x✝ x✝¹ : CategoryTheory.Limits.WalkingParallelFamily.Hom J✝ a✝ a✝¹) : Decidable (x✝ = x✝¹)
• CategoryTheory.Limits.hasWideCoequalizers_of_hasColimit_parallelFamily 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelFamily f)] : CategoryTheory.Limits.HasWideCoequalizers C
• CategoryTheory.Limits.hasWideEqualizers_of_hasLimit_parallelFamily 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (C : Type u) [CategoryTheory.Category.{v, u} C] [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelFamily f)] : CategoryTheory.Limits.HasWideEqualizers C
• CategoryTheory.Limits.parallelFamily_obj_one 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) : (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.one = Y
• CategoryTheory.Limits.parallelFamily_obj_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) : (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.zero = X
• CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (x : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.functor.obj x = CategoryTheory.Limits.WalkingParallelFamily.rec CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one x
• CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_obj 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (x : CategoryTheory.Limits.WalkingParallelPair) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.inverse.obj x = CategoryTheory.Limits.parallelPair.parallelPairObj CategoryTheory.Limits.WalkingParallelFamily.zero CategoryTheory.Limits.WalkingParallelFamily.one x
• CategoryTheory.Limits.Cocone.ofCotrident 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cotrident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) : CategoryTheory.Limits.Cocone F
• CategoryTheory.Limits.Cone.ofTrident 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Trident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) : CategoryTheory.Limits.Cone F
• CategoryTheory.Limits.Cotrident.ofCocone 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cotrident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)
• CategoryTheory.Limits.Trident.ofCone 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cone F) : CategoryTheory.Limits.Trident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)
• CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv_functor 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {J' : Type w'} (e : J ≃ J') : (CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv e).functor = CategoryTheory.Limits.parallelFamily fun j => CategoryTheory.Limits.WalkingParallelFamily.Hom.line (e j)
• CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv_inverse 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {J' : Type w'} (e : J ≃ J') : (CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv e).inverse = CategoryTheory.Limits.parallelFamily fun j => CategoryTheory.Limits.WalkingParallelFamily.Hom.line (e.symm j)
• CategoryTheory.Limits.diagramIsoParallelFamily 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C) : F ≅ CategoryTheory.Limits.parallelFamily fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)
• CategoryTheory.Limits.wideCoequalizerIsWideCoequalizer 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cotrident.ofπ (CategoryTheory.Limits.wideCoequalizer.π f) ⋯)
• CategoryTheory.Limits.wideEqualizerIsWideEqualizer 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] [Nonempty J] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Trident.ofι (CategoryTheory.Limits.wideEqualizer.ι f) ⋯)
• CategoryTheory.Limits.parallelFamily_map_left 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) {j : J} : (CategoryTheory.Limits.parallelFamily f).map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j) = f j
• CategoryTheory.Limits.Cotrident.ofπ_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (π : Y ⟶ P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) : (CategoryTheory.Limits.Cotrident.ofπ π w).pt = P
• CategoryTheory.Limits.Trident.ofι_pt 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (ι : P ⟶ X) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) : (CategoryTheory.Limits.Trident.ofι ι w).pt = P
• CategoryTheory.Limits.Cotrident.π 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (t : CategoryTheory.Limits.Cotrident f) : (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.one ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one
• CategoryTheory.Limits.Trident.ι 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (t : CategoryTheory.Limits.Trident f) : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.zero ⟶ (CategoryTheory.Limits.parallelFamily f).obj CategoryTheory.Limits.WalkingParallelFamily.zero
• CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_map 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {X✝ Y✝ : CategoryTheory.Limits.WalkingParallelPair} (h : X✝ ⟶ Y✝) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.inverse.map h = CategoryTheory.Limits.parallelPair.parallelPairHom (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := true }) (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := false }) h
• CategoryTheory.Limits.Cotrident.IsColimit.homIso 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Cotrident f} (ht : CategoryTheory.Limits.IsColimit t) (Z : C) : (t.pt ⟶ Z) ≃ { h // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) h = CategoryTheory.CategoryStruct.comp (f j₂) h }
• CategoryTheory.Limits.Trident.IsLimit.homIso 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) : (Z ⟶ t.pt) ≃ { h // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp h (f j₁) = CategoryTheory.CategoryStruct.comp h (f j₂) }
• CategoryTheory.Limits.mono_of_isLimit_parallelFamily 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {c : CategoryTheory.Limits.Cone (CategoryTheory.Limits.parallelFamily f)} (i : CategoryTheory.Limits.IsLimit c) : CategoryTheory.Mono (CategoryTheory.Limits.Trident.ι c)
• CategoryTheory.Limits.wideCoequalizer.cotrident_π 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] : (CategoryTheory.Limits.wideCoequalizer.cotrident f).π = CategoryTheory.Limits.wideCoequalizer.π f
• CategoryTheory.Limits.wideEqualizer.trident_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] : (CategoryTheory.Limits.wideEqualizer.trident f).ι = CategoryTheory.Limits.wideEqualizer.ι f
• CategoryTheory.Limits.Cotrident.π_ofπ 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (π : Y ⟶ P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) : (CategoryTheory.Limits.Cotrident.ofπ π w).π = π
• CategoryTheory.Limits.Trident.ι_ofι 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (ι : P ⟶ X) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) : (CategoryTheory.Limits.Trident.ofι ι w).ι = ι
• CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_functor_map 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {x y : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)} (h : x ⟶ y) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.functor.map h = match x, y, h with | x, .(x), CategoryTheory.Limits.WalkingParallelFamily.Hom.id .(x) => CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.WalkingParallelFamily.rec CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.WalkingParallelPair.one x) | .(CategoryTheory.Limits.WalkingParallelFamily.zero), .(CategoryTheory.Limits.WalkingParallelFamily.one), CategoryTheory.Limits.WalkingParallelFamily.Hom.line j => if j.down = true then CategoryTheory.Limits.WalkingParallelPairHom.left else CategoryTheory.Limits.WalkingParallelPairHom.right
• CategoryTheory.Limits.Cotrident.π_eq_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (t : CategoryTheory.Limits.Cotrident f) : t.π = t.ι.app CategoryTheory.Limits.WalkingParallelFamily.one
• CategoryTheory.Limits.Trident.ι_eq_app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (t : CategoryTheory.Limits.Trident f) : t.ι = t.π.app CategoryTheory.Limits.WalkingParallelFamily.zero
• CategoryTheory.Limits.epi_of_isColimit_parallelFamily 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {c : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.parallelFamily f)} (i : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Epi (c.ι.app CategoryTheory.Limits.WalkingParallelFamily.one)
• CategoryTheory.Limits.wideCoequalizer.cotrident_ι_app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideCoequalizer f] : (CategoryTheory.Limits.wideCoequalizer.cotrident f).ι.app CategoryTheory.Limits.WalkingParallelFamily.one = CategoryTheory.Limits.wideCoequalizer.π f
• CategoryTheory.Limits.wideEqualizer.trident_π_app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y)) [CategoryTheory.Limits.HasWideEqualizer f] : (CategoryTheory.Limits.wideEqualizer.trident f).π.app CategoryTheory.Limits.WalkingParallelFamily.zero = CategoryTheory.Limits.wideEqualizer.ι f
• CategoryTheory.Limits.Trident.IsLimit.lift' 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)) : { l // CategoryTheory.CategoryStruct.comp l s.ι = k }
• CategoryTheory.Limits.Cotrident.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (j₁ j₂ : J) (t : CategoryTheory.Limits.Cotrident f) : CategoryTheory.CategoryStruct.comp (f j₁) t.π = CategoryTheory.CategoryStruct.comp (f j₂) t.π
• CategoryTheory.Limits.Trident.mkHom 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : CategoryTheory.Limits.Trident f} (k : s.pt ⟶ t.pt) (w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι := by cat_disch) : s ⟶ t
• CategoryTheory.Limits.Trident.IsLimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Trident f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} {k l : W ⟶ s.pt} (h : CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι) : k = l
• CategoryTheory.Limits.Trident.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : CategoryTheory.Limits.Trident f} (i : s.pt ≅ t.pt) (w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : s ≅ t
• CategoryTheory.Limits.Cotrident.IsColimit.desc' 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Cotrident f} (hs : CategoryTheory.Limits.IsColimit s) {W : C} (k : Y ⟶ W) (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k) : { l // CategoryTheory.CategoryStruct.comp s.π l = k }
• CategoryTheory.Limits.Cotrident.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (j₁ j₂ : J) (t : CategoryTheory.Limits.Cotrident f) {Z : C} (h : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one ⟶ Z) : CategoryTheory.CategoryStruct.comp (f j₁) (CategoryTheory.CategoryStruct.comp t.π h) = CategoryTheory.CategoryStruct.comp (f j₂) (CategoryTheory.CategoryStruct.comp t.π h)
• CategoryTheory.Limits.Trident.condition 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (j₁ j₂ : J) (t : CategoryTheory.Limits.Trident f) : CategoryTheory.CategoryStruct.comp t.ι (f j₁) = CategoryTheory.CategoryStruct.comp t.ι (f j₂)
• CategoryTheory.Limits.Trident.mkHom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : CategoryTheory.Limits.Trident f} (k : s.pt ⟶ t.pt) (w : CategoryTheory.CategoryStruct.comp k t.ι = s.ι := by cat_disch) : (CategoryTheory.Limits.Trident.mkHom k w).hom = k
• CategoryTheory.Limits.Cotrident.mkHom 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : CategoryTheory.Limits.Cotrident f} (k : s.pt ⟶ t.pt) (w : CategoryTheory.CategoryStruct.comp s.π k = t.π := by cat_disch) : s ⟶ t
• CategoryTheory.Limits.diagramIsoParallelFamily_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C) (X : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.diagramIsoParallelFamily F).hom.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.Cotrident.ext 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : CategoryTheory.Limits.Cotrident f} (i : s.pt ≅ t.pt) (w : CategoryTheory.CategoryStruct.comp s.π i.hom = t.π := by cat_disch) : s ≅ t
• CategoryTheory.Limits.Cotrident.app_one 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (s : CategoryTheory.Limits.Cotrident f) (j : J) : CategoryTheory.CategoryStruct.comp (f j) (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.one) = s.ι.app CategoryTheory.Limits.WalkingParallelFamily.zero
• CategoryTheory.Limits.Cotrident.mkHom_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : CategoryTheory.Limits.Cotrident f} (k : s.pt ⟶ t.pt) (w : CategoryTheory.CategoryStruct.comp s.π k = t.π := by cat_disch) : (CategoryTheory.Limits.Cotrident.mkHom k w).hom = k
• CategoryTheory.Limits.Trident.app_zero 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (s : CategoryTheory.Limits.Trident f) (j : J) : CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero) (f j) = s.π.app CategoryTheory.Limits.WalkingParallelFamily.one
• CategoryTheory.Limits.Cotrident.IsColimit.hom_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s : CategoryTheory.Limits.Cotrident f} (hs : CategoryTheory.Limits.IsColimit s) {W : C} {k l : s.pt ⟶ W} (h : CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l) : k = l
• CategoryTheory.Limits.Trident.condition_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (j₁ j₂ : J) (t : CategoryTheory.Limits.Trident f) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp t.ι (CategoryTheory.CategoryStruct.comp (f j₁) h) = CategoryTheory.CategoryStruct.comp t.ι (CategoryTheory.CategoryStruct.comp (f j₂) h)
• CategoryTheory.Limits.Cotrident.ofπ_ι_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (π : Y ⟶ P) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) π = CategoryTheory.CategoryStruct.comp (f j₂) π) (X✝ : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Cotrident.ofπ π w).ι.app X✝ = CategoryTheory.Limits.WalkingParallelFamily.casesOn X✝ (CategoryTheory.CategoryStruct.comp (f (Classical.arbitrary J)) π) π
• CategoryTheory.Limits.Trident.ofι_π_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {P : C} (ι : P ⟶ X) (w : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp ι (f j₁) = CategoryTheory.CategoryStruct.comp ι (f j₂)) (X✝ : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Trident.ofι ι w).π.app X✝ = CategoryTheory.Limits.WalkingParallelFamily.casesOn X✝ ι (CategoryTheory.CategoryStruct.comp ι (f (Classical.arbitrary J)))
• CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (X : CategoryTheory.Limits.WalkingParallelPair) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.counitIso.hom.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.diagramIsoParallelFamily_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C) (X : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.diagramIsoParallelFamily F).inv.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.Trident.ext_hom 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : CategoryTheory.Limits.Trident f} (i : s.pt ≅ t.pt) (w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : (CategoryTheory.Limits.Trident.ext i w).hom = CategoryTheory.Limits.Trident.mkHom i.hom w
• CategoryTheory.Limits.Trident.ext_inv 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {s t : CategoryTheory.Limits.Trident f} (i : s.pt ≅ t.pt) (w : CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι := by cat_disch) : (CategoryTheory.Limits.Trident.ext i w).inv = CategoryTheory.Limits.Trident.mkHom i.inv ⋯
• CategoryTheory.Limits.Cotrident.app_one_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (s : CategoryTheory.Limits.Cotrident f) (j : J) {Z : C} (h : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one ⟶ Z) : CategoryTheory.CategoryStruct.comp (f j) (CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.one) h) = CategoryTheory.CategoryStruct.comp (s.ι.app CategoryTheory.Limits.WalkingParallelFamily.zero) h
• CategoryTheory.Limits.Trident.app_zero_assoc 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (s : CategoryTheory.Limits.Trident f) (j : J) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero) (CategoryTheory.CategoryStruct.comp (f j) h) = CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.one) h
• CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_counitIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (X : CategoryTheory.Limits.WalkingParallelPair) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.counitIso.inv.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_hom_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (X : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.unitIso.hom.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv_unitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {J' : Type w'} (e : J ≃ J') : (CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv e).unitIso = CategoryTheory.NatIso.ofComponents (fun x => match x with | CategoryTheory.Limits.WalkingParallelFamily.zero => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.WalkingParallelFamily J)).obj CategoryTheory.Limits.WalkingParallelFamily.zero) | CategoryTheory.Limits.WalkingParallelFamily.one => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.WalkingParallelFamily J)).obj CategoryTheory.Limits.WalkingParallelFamily.one)) ⋯
• CategoryTheory.Limits.Trident.equalizer_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] (s : CategoryTheory.Limits.Trident f) {W : C} {k l : W ⟶ s.pt} (h : CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι) (j : CategoryTheory.Limits.WalkingParallelFamily J) : CategoryTheory.CategoryStruct.comp k (s.π.app j) = CategoryTheory.CategoryStruct.comp l (s.π.app j)
• CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_unitIso_inv_app 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  (X : CategoryTheory.Limits.WalkingParallelFamily (ULift.{w, 0} Bool)) : CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.unitIso.inv.app X = CategoryTheory.eqToHom ⋯
• CategoryTheory.Limits.Trident.IsLimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] (t : CategoryTheory.Limits.Trident f) (lift : (s : CategoryTheory.Limits.Trident f) → s.pt ⟶ t.pt) (fac : ∀ (s : CategoryTheory.Limits.Trident f), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι) (uniq : ∀ (s : CategoryTheory.Limits.Trident f) (m : s.pt ⟶ t.pt), (∀ (j : CategoryTheory.Limits.WalkingParallelFamily J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift s) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv_counitIso 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {J' : Type w'} (e : J ≃ J') : (CategoryTheory.Limits.WalkingParallelFamily.equivalenceOfEquiv e).counitIso = CategoryTheory.NatIso.ofComponents (fun x => match x with | CategoryTheory.Limits.WalkingParallelFamily.zero => CategoryTheory.Iso.refl (((CategoryTheory.Limits.parallelFamily fun j => CategoryTheory.Limits.WalkingParallelFamily.Hom.line (e.symm j)).comp (CategoryTheory.Limits.parallelFamily fun j => CategoryTheory.Limits.WalkingParallelFamily.Hom.line (e j))).obj CategoryTheory.Limits.WalkingParallelFamily.zero) | CategoryTheory.Limits.WalkingParallelFamily.one => CategoryTheory.Iso.refl (((CategoryTheory.Limits.parallelFamily fun j => CategoryTheory.Limits.WalkingParallelFamily.Hom.line (e.symm j)).comp (CategoryTheory.Limits.parallelFamily fun j => CategoryTheory.Limits.WalkingParallelFamily.Hom.line (e j))).obj CategoryTheory.Limits.WalkingParallelFamily.one)) ⋯
• CategoryTheory.Limits.Cocone.ofCotrident_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cotrident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) (j : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Cocone.ofCotrident t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
• CategoryTheory.Limits.Cone.ofTrident_π 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Trident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) (j : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Cone.ofTrident t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Limits.Cotrident.coequalizer_ext 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] (s : CategoryTheory.Limits.Cotrident f) {W : C} {k l : s.pt ⟶ W} (h : CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l) (j : CategoryTheory.Limits.WalkingParallelFamily J) : CategoryTheory.CategoryStruct.comp (s.ι.app j) k = CategoryTheory.CategoryStruct.comp (s.ι.app j) l
• CategoryTheory.Limits.Cotrident.ofCocone_ι 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cocone F) (j : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Cotrident.ofCocone t).ι.app j = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (t.ι.app j)
• CategoryTheory.Limits.Trident.ofCone_π 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} (t : CategoryTheory.Limits.Cone F) (j : CategoryTheory.Limits.WalkingParallelFamily J) : (CategoryTheory.Limits.Trident.ofCone t).π.app j = CategoryTheory.CategoryStruct.comp (t.π.app j) (CategoryTheory.eqToHom ⋯)
• CategoryTheory.Limits.Cotrident.IsColimit.mk 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] (t : CategoryTheory.Limits.Cotrident f) (desc : (s : CategoryTheory.Limits.Cotrident f) → t.pt ⟶ s.pt) (fac : ∀ (s : CategoryTheory.Limits.Cotrident f), CategoryTheory.CategoryStruct.comp t.π (desc s) = s.π) (uniq : ∀ (s : CategoryTheory.Limits.Cotrident f) (m : t.pt ⟶ s.pt), (∀ (j : CategoryTheory.Limits.WalkingParallelFamily J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc s) : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Limits.Trident.IsLimit.homIso_apply_coe 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) (k : Z ⟶ t.pt) : ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp k t.ι
• CategoryTheory.Limits.Cotrident.IsColimit.homIso_apply_coe 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Cotrident f} (ht : CategoryTheory.Limits.IsColimit t) (Z : C) (k : t.pt ⟶ Z) : ↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z) k) = CategoryTheory.CategoryStruct.comp t.π k
• CategoryTheory.Limits.Cotrident.IsColimit.mk' 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] (t : CategoryTheory.Limits.Cotrident f) (create : (s : CategoryTheory.Limits.Cotrident f) → { l // CategoryTheory.CategoryStruct.comp t.π l = s.π ∧ ∀ {m : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj CategoryTheory.Limits.WalkingParallelFamily.one}, CategoryTheory.CategoryStruct.comp t.π m = s.π → m = l }) : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Limits.Trident.IsLimit.mk' 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] (t : CategoryTheory.Limits.Trident f) (create : (s : CategoryTheory.Limits.Trident f) → { l // CategoryTheory.CategoryStruct.comp l t.ι = s.ι ∧ ∀ {m : ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj s.pt).obj CategoryTheory.Limits.WalkingParallelFamily.zero ⟶ ((CategoryTheory.Functor.const (CategoryTheory.Limits.WalkingParallelFamily J)).obj t.pt).obj CategoryTheory.Limits.WalkingParallelFamily.zero}, CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = l }) : CategoryTheory.Limits.IsLimit t
• CategoryTheory.Limits.Trident.IsLimit.homIso_symm_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) (Z : C) (h : { h // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp h (f j₁) = CategoryTheory.CategoryStruct.comp h (f j₂) }) : (CategoryTheory.Limits.Trident.IsLimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Trident.IsLimit.lift' ht ↑h ⋯)
• CategoryTheory.Limits.Cotrident.IsColimit.homIso_symm_apply 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Cotrident f} (ht : CategoryTheory.Limits.IsColimit t) (Z : C) (h : { h // ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) h = CategoryTheory.CategoryStruct.comp (f j₂) h }) : (CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Cotrident.IsColimit.desc' ht ↑h ⋯)
• CategoryTheory.Limits.Cotrident.IsColimit.homIso_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Cotrident f} {Z Z' : C} (q : Z ⟶ Z') (ht : CategoryTheory.Limits.IsColimit t) (k : t.pt ⟶ Z) : ↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp k q)) = CategoryTheory.CategoryStruct.comp (↑((CategoryTheory.Limits.Cotrident.IsColimit.homIso ht Z) k)) q
• CategoryTheory.Limits.Trident.IsLimit.homIso_natural 📋 Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
  {J : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J] {t : CategoryTheory.Limits.Trident f} (ht : CategoryTheory.Limits.IsLimit t) {Z Z' : C} (q : Z' ⟶ Z) (k : Z ⟶ t.pt) : ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z') (CategoryTheory.CategoryStruct.comp q k)) = CategoryTheory.CategoryStruct.comp q ↑((CategoryTheory.Limits.Trident.IsLimit.homIso ht Z) k)
• CategoryTheory.hasCardinalLT_arrow_walkingParallelFamily 📋 Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
  {T : Type u} {κ : Cardinal.{w}} (hT : HasCardinalLT T κ) (hκ : Cardinal.aleph0 ≤ κ) : HasCardinalLT (CategoryTheory.Arrow (CategoryTheory.Limits.WalkingParallelFamily T)) κ

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