Theorems · Definition · category theory

CategoryTheory.Limits.WidePullback.base

{J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {B : C} →
        {objs : J → C} →
          (arrows : (j : J) → objs j ⟶ B) →
            [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] →
              CategoryTheory.Limits.widePullback B objs arrows ⟶ B

The unique map to the base from the pullback.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Cited by

20 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasWidePullback