Theorems · Definition · category theory

CategoryTheory.Over.ConstructProducts.conesEquivInverse

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (B : C) →
      {J : Type w} →
        (F : CategoryTheory.Functor (CategoryTheory.Discrete J) (CategoryTheory.Over B)) →
          CategoryTheory.Functor (CategoryTheory.Limits.Cone F)
            (CategoryTheory.Limits.Cone (CategoryTheory.Over.ConstructProducts.widePullbackDiagramOfDiagramOver B F))

(Impl) A preliminary definition to avoid timeouts.

Defined in

Mathlib.CategoryTheory.Limits.Constructions.Over.Products

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category