Theorems · Inductive type · category theory

CategoryTheory.SmallObject.FunctorObjIndex

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} → {A B : I → C} → ((i : I) → A i ⟶ B i) → {S X : C} → (X ⟶ S) → Type (max v w)

Given a family of morphisms f i : A i ⟶ B i and a morphism πX : X ⟶ S, this type parametrizes the commutative squares with a morphism f i on the left and πX on the right.

Defined in

Mathlib.CategoryTheory.SmallObject.Construction

Cited by

46 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.Category