Theorems · Inductive type · category theory

CategoryTheory.PrelaxFunctorStruct

(B : Type u₁) →
  [inst : Quiver B] →
    [(a b : B) → Quiver (a ⟶ b)] →
      (C : Type u₂) →
        [inst : Quiver C] → [(a b : C) → Quiver (a ⟶ b)] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)

A PrelaxFunctorStruct between bicategories consists of functions between objects, 1-morphisms, and 2-morphisms. This structure will be extended to define PrelaxFunctor.

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Prelax

Cited by

11 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

QuiverQuiverQuiverQuiver