Theorems · Definition · category theory

CategoryTheory.Functor.Final.induction

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Final] →
            {d : D} →
              (Z : (X : C) → (d ⟶ F.obj X) → Sort u_1) →
                ((X₁ X₂ : C) →
                    (k₁ : d ⟶ F.obj X₁) →
                      (k₂ : d ⟶ F.obj X₂) →
                        (f : X₁ ⟶ X₂) → CategoryTheory.CategoryStruct.comp k₁ (F.map f) = k₂ → Z X₁ k₁ → Z X₂ k₂) →
                  ((X₁ X₂ : C) →
                      (k₁ : d ⟶ F.obj X₁) →
                        (k₂ : d ⟶ F.obj X₂) →
                          (f : X₁ ⟶ X₂) → CategoryTheory.CategoryStruct.comp k₁ (F.map f) = k₂ → Z X₂ k₂ → Z X₁ k₁) →
                    {X₀ : C} →
                      {k₀ : d ⟶ F.obj X₀} →
                        Z X₀ k₀ → Z (CategoryTheory.Functor.Final.lift F d) (CategoryTheory.Functor.Final.homToLift F d)

We provide an induction principle for reasoning about lift and homToLift. We want to perform some construction (usually just a proof) about the particular choices lift F d and homToLift F d, it suffices to perform that construction for some other pair of choices (denoted X₀ : C and k₀ : d ⟶ F.obj X₀ below), and to show how to transport such a construction both directions along a morphism between such choices.

Defined in

Mathlib.CategoryTheory.Limits.Final

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.Final