Theorems · Definition · category theory

CategoryTheory.ReflPrefunctor.mk.noConfusion

{V : Type u₁} →
  {inst : CategoryTheory.ReflQuiver V} →
    {W : Type u₂} →
      {inst_1 : CategoryTheory.ReflQuiver W} →
        {P : Sort u} →
          {toPrefunctor : V ⥤q W} →
            {map_id :
                autoParam
                  (∀ (X : V),
                    toPrefunctor.map (CategoryTheory.ReflQuiver.id X) =
                      CategoryTheory.ReflQuiver.id (toPrefunctor.obj X))
                  CategoryTheory.ReflPrefunctor.map_id._autoParam} →
              {toPrefunctor' : V ⥤q W} →
                {map_id' :
                    autoParam
                      (∀ (X : V),
                        toPrefunctor'.map (CategoryTheory.ReflQuiver.id X) =
                          CategoryTheory.ReflQuiver.id (toPrefunctor'.obj X))
                      CategoryTheory.ReflPrefunctor.map_id._autoParam} →
                  { toPrefunctor := toPrefunctor, map_id := map_id } =
                      { toPrefunctor := toPrefunctor', map_id := map_id' } →
                    (toPrefunctor ≍ toPrefunctor' → P) → P

Defined in

Mathlib.Combinatorics.Quiver.ReflQuiver

Cited by

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms