# 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 #

• FreeBicategory B: the free bicategory over a quiver B.
• FreeBicategory.lift F: the pseudofunctor from FreeBicategory B to C associated with a prefunctor F from B to C.

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

Equations
Instances For
inductive CategoryTheory.FreeBicategory.Hom {B : Type u} [] :
BBType (max u v)

1-morphisms in the free bicategory.

• of: {B : Type u} → [inst : ] → {a b : B} → (a b)
• id: {B : Type u} → [inst : ] → (a : B) →
• comp: {B : Type u} → [inst : ] → {a b c : B} →
Instances For
instance CategoryTheory.FreeBicategory.instInhabitedHom {B : Type u} [] (a : B) (b : B) [Inhabited (a b)] :
Equations
• = { default := }
Equations
• CategoryTheory.FreeBicategory.quiver = { Hom := fun (a b : B) => }
Equations
• One or more equations did not get rendered due to their size.
inductive CategoryTheory.FreeBicategory.Hom₂ {B : Type u} [] :
(a b)(a b)Type (max u v)

Representatives of 2-morphisms in the free bicategory.

• id: {B : Type u} → [inst : ] → {a b : } → (f : a b) →
• vcomp: {B : Type u} → [inst : ] → {a b : } → {f g h : a b} →
• whisker_left: {B : Type u} → [inst : ] → {a b c : } → (f : a b) → {g h : b c} →
• whisker_right: {B : Type u} → [inst : ] → {a b c : } → {f g : a b} → (h : b c) →
• associator: {B : Type u} → [inst : ] → {a b c d : } → (f : a b) → (g : b c) → (h : c d) →
• associator_inv: {B : Type u} → [inst : ] → {a b c d : } → (f : a b) → (g : b c) → (h : c d) →
• right_unitor: {B : Type u} → [inst : ] → {a b : } →
• right_unitor_inv: {B : Type u} → [inst : ] → {a b : } →
• left_unitor: {B : Type u} → [inst : ] → {a b : } →
• left_unitor_inv: {B : Type u} → [inst : ] → {a b : } →
Instances For
inductive CategoryTheory.FreeBicategory.Rel {B : Type u} [] {f : a b} {g : a b} :

Relations between 2-morphisms in the free bicategory.

• vcomp_right: ∀ {B : Type u} [inst : ] {a b : B} {f g h : } (η : ) (θ₁ θ₂ : ),
• vcomp_left: ∀ {B : Type u} [inst : ] {a b : B} {f g h : } (η₁ η₂ : ) (θ : ),
• id_comp: ∀ {B : Type u} [inst : ] {a b : B} {f g : } (η : ),
• comp_id: ∀ {B : Type u} [inst : ] {a b : B} {f g : } (η : ),
• assoc: ∀ {B : Type u} [inst : ] {a b : B} {f g h i : } (η : ) (θ : ) (ι : ),
• whisker_left: ∀ {B : Type u} [inst : ] {a b c : B} (f : ) (g h : ) (η η' : ),
• whisker_left_id: ∀ {B : Type u} [inst : ] {a b c : B} (f : ) (g : ),
• whisker_left_comp: ∀ {B : Type u} [inst : ] {a b c : B} (f : ) {g h i : } (η : ) (θ : ),
• id_whisker_left:
• comp_whisker_left: ∀ {B : Type u} [inst : ] {a b c d : B} (f : ) (g : ) {h h' : } (η : ),
• whisker_right: ∀ {B : Type u} [inst : ] {a b c : B} (f g : ) (h : ) (η η' : ),
• id_whisker_right: ∀ {B : Type u} [inst : ] {a b c : B} (f : ) (g : ),
• comp_whisker_right: ∀ {B : Type u} [inst : ] {a b c : B} {f g h : } (i : ) (η : ) (θ : ),
• whisker_right_id:
• whisker_right_comp: ∀ {B : Type u} [inst : ] {a b c d : B} {f f' : } (g : ) (h : ) (η : ),
• whisker_assoc: ∀ {B : Type u} [inst : ] {a b c d : B} (f : ) {g g' : } (η : ) (h : ),
• whisker_exchange: ∀ {B : Type u} [inst : ] {a b c : B} {f g : } {h i : } (η : ) (θ : ),
• associator_hom_inv: ∀ {B : Type u} [inst : ] {a b c d : B} (f : ) (g : ) (h : ),
• associator_inv_hom: ∀ {B : Type u} [inst : ] {a b c d : B} (f : ) (g : ) (h : ),
• left_unitor_hom_inv: ∀ {B : Type u} [inst : ] {a b : B} (f : ),
• left_unitor_inv_hom: ∀ {B : Type u} [inst : ] {a b : B} (f : ),
• right_unitor_hom_inv:
• right_unitor_inv_hom: ∀ {B : Type u} [inst : ] {a b : B} (f : ),
• pentagon: ∀ {B : Type u} [inst : ] {a b c d e : B} (f : ) (g : ) (h : ) (i : ),
• triangle:
Instances For

Bicategory structure on the free bicategory.

Equations
• One or more equations did not get rendered due to their size.
@[inline, reducible]
abbrev CategoryTheory.FreeBicategory.Hom₂.mk {B : Type u} [] {f : a b} {g : a b} (η : ) :
f g
Equations
• = Quot.mk CategoryTheory.FreeBicategory.Rel η
Instances For
@[simp]
theorem CategoryTheory.FreeBicategory.mk_vcomp {B : Type u} [] {f : a b} {g : a b} {h : a b} (η : ) (θ : ) :
@[simp]
theorem CategoryTheory.FreeBicategory.mk_whisker_left {B : Type u} [] (f : a b) {g : b c} {h : b c} (η : ) :
@[simp]
theorem CategoryTheory.FreeBicategory.mk_whisker_right {B : Type u} [] {f : a b} {g : a b} (η : ) (h : b c) :
theorem CategoryTheory.FreeBicategory.comp_def {B : Type u} [] (f : a b) (g : b c) :
@[simp]
theorem CategoryTheory.FreeBicategory.mk_id {B : Type u} [] (f : a b) :
Quot.mk CategoryTheory.FreeBicategory.Rel =
@[simp]
theorem CategoryTheory.FreeBicategory.mk_associator_hom {B : Type u} [] (f : a b) (g : b c) (h : c d) :
Quot.mk CategoryTheory.FreeBicategory.Rel = .hom
@[simp]
theorem CategoryTheory.FreeBicategory.mk_associator_inv {B : Type u} [] (f : a b) (g : b c) (h : c d) :
Quot.mk CategoryTheory.FreeBicategory.Rel = .inv
@[simp]
theorem CategoryTheory.FreeBicategory.mk_left_unitor_hom {B : Type u} [] (f : a b) :
Quot.mk CategoryTheory.FreeBicategory.Rel =
@[simp]
theorem CategoryTheory.FreeBicategory.mk_left_unitor_inv {B : Type u} [] (f : a b) :
Quot.mk CategoryTheory.FreeBicategory.Rel =
@[simp]
theorem CategoryTheory.FreeBicategory.mk_right_unitor_hom {B : Type u} [] (f : a b) :
Quot.mk CategoryTheory.FreeBicategory.Rel =
@[simp]
theorem CategoryTheory.FreeBicategory.mk_right_unitor_inv {B : Type u} [] (f : a b) :
Quot.mk CategoryTheory.FreeBicategory.Rel =
@[simp]
theorem CategoryTheory.FreeBicategory.of_obj {B : Type u} [] (a : B) :
CategoryTheory.FreeBicategory.of.obj a = id a
@[simp]
theorem CategoryTheory.FreeBicategory.of_map {B : Type u} [] :
∀ (x x_1 : B) (f : x x_1), CategoryTheory.FreeBicategory.of.map f =

Canonical prefunctor from B to free_bicategory B.

Equations
• CategoryTheory.FreeBicategory.of = { obj := id, map := fun (x x_1 : B) => CategoryTheory.FreeBicategory.Hom.of }
Instances For
def CategoryTheory.FreeBicategory.liftHom {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) :
(a b)(F.obj a F.obj b)

Auxiliary definition for lift.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.FreeBicategory.liftHom_id {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) :
@[simp]
theorem CategoryTheory.FreeBicategory.liftHom_comp {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) (f : a b) (g : b c) :
def CategoryTheory.FreeBicategory.liftHom₂ {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) {f : a b} {g : a b} :

Auxiliary definition for lift.

Instances For
theorem CategoryTheory.FreeBicategory.liftHom₂_congr {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) {f : a b} {g : a b} {η : } {θ : } (H : ) :
@[simp]
theorem CategoryTheory.FreeBicategory.lift_mapId {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) :
.mapId a = CategoryTheory.Iso.refl ({ toPrefunctor := { obj := F.obj, map := fun {X Y : } => }, map₂ := fun {a b : } {f g : a b} => }.map )
@[simp]
theorem CategoryTheory.FreeBicategory.lift_mapComp {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) :
∀ {a b c : } (f : a b) (g : b c), .mapComp f g = CategoryTheory.Iso.refl ({ toPrefunctor := { obj := F.obj, map := fun {X Y : } => }, map₂ := fun {a b : } {f g : a b} => }.map )
@[simp]
theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrefunctor_map {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) :
∀ {X Y : } (a : X Y),
@[simp]
theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_map₂ {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) :
∀ {a b : } {f g : a b} (a_1 : Quot CategoryTheory.FreeBicategory.Rel), .map₂ a_1 =
@[simp]
theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrefunctor_obj {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) :
∀ (a : B), a = F.obj a
def CategoryTheory.FreeBicategory.lift {B : Type u₁} [] {C : Type u₂} (F : B ⥤q C) :

A prefunctor from a quiver B to a bicategory C can be lifted to a pseudofunctor from free_bicategory B to C.

Equations
• One or more equations did not get rendered due to their size.
Instances For