mathlib3 documentation

Free bicategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define the free bicategory over a quiver. In this bicategory, the 1-morphisms are freely generated by the arrows in the quiver, and the 2-morphisms are freely generated by the formal identities, the formal unitors, and the formal associators modulo the relation derived from the axioms of a bicategory.

Main definitions #

Free bicategory over a quiver. Its objects are the same as those in the underlying quiver.

Instances for category_theory.free_bicategory
inductive category_theory.free_bicategory.hom {B : Type u} [quiver B] :
B B Type (max u v)

1-morphisms in the free bicategory.

Instances for category_theory.free_bicategory.hom

Representatives of 2-morphisms in the free bicategory.

Instances for category_theory.free_bicategory.hom₂
  • category_theory.free_bicategory.hom₂.has_sizeof_inst

Relations between 2-morphisms in the free bicategory.

@[protected, instance]

Bicategory structure on the free bicategory.


Canonical prefunctor from B to free_bicategory B.


Auxiliary definition for lift.

theorem category_theory.free_bicategory.lift_obj {B : Type u₁} [quiver B] {C : Type u₂} [category_theory.bicategory C] (F : B ⥤q C) (ᾰ : B) :