Theorems · Definition · category theory

CategoryTheory.PrelaxFunctorStruct.mk.noConfusion

{B : Type u₁} →
  {inst : Quiver B} →
    {inst_1 : (a b : B) → Quiver (a ⟶ b)} →
      {C : Type u₂} →
        {inst_2 : Quiver C} →
          {inst_3 : (a b : C) → Quiver (a ⟶ b)} →
            {P : Sort u} →
              {toPrefunctor : B ⥤q C} →
                {map₂ : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor.map f ⟶ toPrefunctor.map g)} →
                  {toPrefunctor' : B ⥤q C} →
                    {map₂' : {a b : B} → {f g : a ⟶ b} → (f ⟶ g) → (toPrefunctor'.map f ⟶ toPrefunctor'.map g)} →
                      { toPrefunctor := toPrefunctor, map₂ := map₂ } =
                          { toPrefunctor := toPrefunctor', map₂ := map₂' } →
                        (toPrefunctor ≍ toPrefunctor' → map₂ ≍ map₂' → P) → P

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms