mathlib documentation

Free bicategories #

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 #

def category_theory.free_bicategory (B : Type u) :
Type u

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
inductive category_theory.free_bicategory.hom₂ {B : Type u} [quiver B] {a b : B} :

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 : prefunctor B C) (ᾰ : B) :