Theorems · Definition · category theory

CategoryTheory.Dial.Hom.recOn

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        {X Y : CategoryTheory.Dial C} →
          {motive : X.Hom Y → Sort u_1} →
            (t : X.Hom Y) →
              ((f : X.src ⟶ Y.src) →
                  (F : X.src ⨯ Y.tgt ⟶ X.tgt) →
                    (le :
                        (CategoryTheory.Subobject.pullback
                                (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst F)).obj
                            X.rel ≤
                          (CategoryTheory.Subobject.pullback
                                (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id Y.tgt))).obj
                            Y.rel) →
                      motive { f := f, F := F, le := le }) →
                motive t

Defined in

Mathlib.CategoryTheory.Dialectica.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasFiniteProductsCategoryTheory.Limits.HasPullbacks