Documentation

Mathlib.CategoryTheory.Bicategory.Free

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.

def CategoryTheory.FreeBicategory (B : Type u) :

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

Equations

CategoryTheory.FreeBicategory B = B

Instances For

instance CategoryTheory.instInhabitedFreeBicategory (B : Type u) [Inhabited B] :

Inhabited (CategoryTheory.FreeBicategory B)

Equations

CategoryTheory.instInhabitedFreeBicategory B = id h

inductive CategoryTheory.FreeBicategory.Hom {B : Type u} [Quiver B] :

B → B → Type (max u v)

1-morphisms in the free bicategory.

of {B : Type u} [Quiver B] {a b : B} (f : a ⟶ b) : CategoryTheory.FreeBicategory.Hom a b
id {B : Type u} [Quiver B] (a : B) : CategoryTheory.FreeBicategory.Hom a a
comp {B : Type u} [Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c) : CategoryTheory.FreeBicategory.Hom a c

Instances For

instance CategoryTheory.FreeBicategory.instInhabitedHomOfHom {B : Type u} [Quiver B] (a b : B) [Inhabited (a ⟶ b)] :

Inhabited (CategoryTheory.FreeBicategory.Hom a b)

Equations

CategoryTheory.FreeBicategory.instInhabitedHomOfHom a b = { default := CategoryTheory.FreeBicategory.Hom.of default }

instance CategoryTheory.FreeBicategory.quiver {B : Type u} [Quiver B] :

Quiver (CategoryTheory.FreeBicategory B)

Equations

CategoryTheory.FreeBicategory.quiver = { Hom := fun (a b : B) => CategoryTheory.FreeBicategory.Hom a b }

instance CategoryTheory.FreeBicategory.categoryStruct {B : Type u} [Quiver B] :

CategoryTheory.CategoryStruct.{max u v, u} (CategoryTheory.FreeBicategory B)

Equations

One or more equations did not get rendered due to their size.

inductive CategoryTheory.FreeBicategory.Hom₂ {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} :

(a ⟶ b) → (a ⟶ b) → Type (max u v)

Representatives of 2-morphisms in the free bicategory.

id {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) : CategoryTheory.FreeBicategory.Hom₂ f f
vcomp {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} {f g h : a ⟶ b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h) : CategoryTheory.FreeBicategory.Hom₂ f h
whisker_left {B : Type u} [Quiver B] {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : CategoryTheory.FreeBicategory.Hom₂ g h) : CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f h)
whisker_right {B : Type u} [Quiver B] {a b c : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} (h : b ⟶ c) (η : CategoryTheory.FreeBicategory.Hom₂ f g) : CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.FreeBicategory.Hom.comp f h) (CategoryTheory.FreeBicategory.Hom.comp g h)
associator {B : Type u} [Quiver B] {a b c d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
associator_inv {B : Type u} [Quiver B] {a b c d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)
right_unitor {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) : CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) f
right_unitor_inv {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) : CategoryTheory.FreeBicategory.Hom₂ f (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))
left_unitor {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) : CategoryTheory.FreeBicategory.Hom₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) f
left_unitor_inv {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) : CategoryTheory.FreeBicategory.Hom₂ f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f)

Instances For

inductive CategoryTheory.FreeBicategory.Rel {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} :

CategoryTheory.FreeBicategory.Hom₂ f g → CategoryTheory.FreeBicategory.Hom₂ f g → Prop

Relations between 2-morphisms in the free bicategory.

vcomp_right {B : Type u} [Quiver B] {a b : B} {f g h : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ₁ θ₂ : CategoryTheory.FreeBicategory.Hom₂ g h) : CategoryTheory.FreeBicategory.Rel θ₁ θ₂ → CategoryTheory.FreeBicategory.Rel (η.vcomp θ₁) (η.vcomp θ₂)
vcomp_left {B : Type u} [Quiver B] {a b : B} {f g h : CategoryTheory.FreeBicategory.Hom a b} (η₁ η₂ : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h) : CategoryTheory.FreeBicategory.Rel η₁ η₂ → CategoryTheory.FreeBicategory.Rel (η₁.vcomp θ) (η₂.vcomp θ)
id_comp {B : Type u} [Quiver B] {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.id f).vcomp η) η
comp_id {B : Type u} [Quiver B] {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) : CategoryTheory.FreeBicategory.Rel (η.vcomp (CategoryTheory.FreeBicategory.Hom₂.id g)) η
assoc {B : Type u} [Quiver B] {a b : B} {f g h i : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h) (ι : CategoryTheory.FreeBicategory.Hom₂ h i) : CategoryTheory.FreeBicategory.Rel ((η.vcomp θ).vcomp ι) (η.vcomp (θ.vcomp ι))
whisker_left {B : Type u} [Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g h : CategoryTheory.FreeBicategory.Hom b c) (η η' : CategoryTheory.FreeBicategory.Hom₂ g h) : CategoryTheory.FreeBicategory.Rel η η' → CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η) (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η')
whisker_left_id {B : Type u} [Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c) : CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.id g)) (CategoryTheory.FreeBicategory.Hom₂.id (f.comp g))
whisker_left_comp {B : Type u} [Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) {g h i : CategoryTheory.FreeBicategory.Hom b c} (η : CategoryTheory.FreeBicategory.Hom₂ g h) (θ : CategoryTheory.FreeBicategory.Hom₂ h i) : CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_left f (η.vcomp θ)) ((CategoryTheory.FreeBicategory.Hom₂.whisker_left f η).vcomp (CategoryTheory.FreeBicategory.Hom₂.whisker_left f θ))
id_whisker_left {B : Type u} [Quiver B] {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) : CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_left (CategoryTheory.FreeBicategory.Hom.id a) η) ((CategoryTheory.FreeBicategory.Hom₂.left_unitor f).vcomp (η.vcomp (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv g)))
comp_whisker_left {B : Type u} [Quiver B] {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c) {h h' : CategoryTheory.FreeBicategory.Hom c d} (η : CategoryTheory.FreeBicategory.Hom₂ h h') : CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_left (f.comp g) η) ((CategoryTheory.FreeBicategory.Hom₂.associator f g h).vcomp ((CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.whisker_left g η)).vcomp (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h')))
whisker_right {B : Type u} [Quiver B] {a b c : B} (f g : CategoryTheory.FreeBicategory.Hom a b) (h : CategoryTheory.FreeBicategory.Hom b c) (η η' : CategoryTheory.FreeBicategory.Hom₂ f g) : CategoryTheory.FreeBicategory.Rel η η' → CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η) (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η')
id_whisker_right {B : Type u} [Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c) : CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right g (CategoryTheory.FreeBicategory.Hom₂.id f)) (CategoryTheory.FreeBicategory.Hom₂.id (f.comp g))
comp_whisker_right {B : Type u} [Quiver B] {a b c : B} {f g h : CategoryTheory.FreeBicategory.Hom a b} (i : CategoryTheory.FreeBicategory.Hom b c) (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h) : CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right i (η.vcomp θ)) ((CategoryTheory.FreeBicategory.Hom₂.whisker_right i η).vcomp (CategoryTheory.FreeBicategory.Hom₂.whisker_right i θ))
whisker_right_id {B : Type u} [Quiver B] {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) : CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right (CategoryTheory.FreeBicategory.Hom.id b) η) ((CategoryTheory.FreeBicategory.Hom₂.right_unitor f).vcomp (η.vcomp (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv g)))
whisker_right_comp {B : Type u} [Quiver B] {a b c d : B} {f f' : CategoryTheory.FreeBicategory.Hom a b} (g : CategoryTheory.FreeBicategory.Hom b c) (h : CategoryTheory.FreeBicategory.Hom c d) (η : CategoryTheory.FreeBicategory.Hom₂ f f') : CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right (g.comp h) η) ((CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h).vcomp ((CategoryTheory.FreeBicategory.Hom₂.whisker_right h (CategoryTheory.FreeBicategory.Hom₂.whisker_right g η)).vcomp (CategoryTheory.FreeBicategory.Hom₂.associator f' g h)))
whisker_assoc {B : Type u} [Quiver B] {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b) {g g' : CategoryTheory.FreeBicategory.Hom b c} (η : CategoryTheory.FreeBicategory.Hom₂ g g') (h : CategoryTheory.FreeBicategory.Hom c d) : CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right h (CategoryTheory.FreeBicategory.Hom₂.whisker_left f η)) ((CategoryTheory.FreeBicategory.Hom₂.associator f g h).vcomp ((CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η)).vcomp (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g' h)))
whisker_exchange {B : Type u} [Quiver B] {a b c : B} {f g : CategoryTheory.FreeBicategory.Hom a b} {h i : CategoryTheory.FreeBicategory.Hom b c} (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ h i) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.whisker_left f θ).vcomp (CategoryTheory.FreeBicategory.Hom₂.whisker_right i η)) ((CategoryTheory.FreeBicategory.Hom₂.whisker_right h η).vcomp (CategoryTheory.FreeBicategory.Hom₂.whisker_left g θ))
associator_hom_inv {B : Type u} [Quiver B] {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c) (h : CategoryTheory.FreeBicategory.Hom c d) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.associator f g h).vcomp (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h)) (CategoryTheory.FreeBicategory.Hom₂.id ((f.comp g).comp h))
associator_inv_hom {B : Type u} [Quiver B] {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c) (h : CategoryTheory.FreeBicategory.Hom c d) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h).vcomp (CategoryTheory.FreeBicategory.Hom₂.associator f g h)) (CategoryTheory.FreeBicategory.Hom₂.id (f.comp (g.comp h)))
left_unitor_hom_inv {B : Type u} [Quiver B] {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.left_unitor f).vcomp (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f)) (CategoryTheory.FreeBicategory.Hom₂.id ((CategoryTheory.FreeBicategory.Hom.id a).comp f))
left_unitor_inv_hom {B : Type u} [Quiver B] {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f).vcomp (CategoryTheory.FreeBicategory.Hom₂.left_unitor f)) (CategoryTheory.FreeBicategory.Hom₂.id f)
right_unitor_hom_inv {B : Type u} [Quiver B] {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.right_unitor f).vcomp (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f)) (CategoryTheory.FreeBicategory.Hom₂.id (f.comp (CategoryTheory.FreeBicategory.Hom.id b)))
right_unitor_inv_hom {B : Type u} [Quiver B] {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f).vcomp (CategoryTheory.FreeBicategory.Hom₂.right_unitor f)) (CategoryTheory.FreeBicategory.Hom₂.id f)
pentagon {B : Type u} [Quiver B] {a b c d e : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c) (h : CategoryTheory.FreeBicategory.Hom c d) (i : CategoryTheory.FreeBicategory.Hom d e) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.whisker_right i (CategoryTheory.FreeBicategory.Hom₂.associator f g h)).vcomp ((CategoryTheory.FreeBicategory.Hom₂.associator f (g.comp h) i).vcomp (CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.associator g h i)))) ((CategoryTheory.FreeBicategory.Hom₂.associator (f.comp g) h i).vcomp (CategoryTheory.FreeBicategory.Hom₂.associator f g (h.comp i)))
triangle {B : Type u} [Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g : CategoryTheory.FreeBicategory.Hom b c) : CategoryTheory.FreeBicategory.Rel ((CategoryTheory.FreeBicategory.Hom₂.associator f (CategoryTheory.FreeBicategory.Hom.id b) g).vcomp (CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.left_unitor g))) (CategoryTheory.FreeBicategory.Hom₂.whisker_right g (CategoryTheory.FreeBicategory.Hom₂.right_unitor f))

Instances For

instance CategoryTheory.FreeBicategory.homCategory {B : Type u} [Quiver B] (a b : CategoryTheory.FreeBicategory B) :

CategoryTheory.Category.{max u v, max u v} (a ⟶ b)

Equations

a.homCategory b = CategoryTheory.Category.mk ⋯ ⋯ ⋯

instance CategoryTheory.FreeBicategory.bicategory {B : Type u} [Quiver B] :

CategoryTheory.Bicategory (CategoryTheory.FreeBicategory B)

Bicategory structure on the free bicategory.

Equations

One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.FreeBicategory.Hom₂.mk {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) :

f ⟶ g

Equations

η.mk = Quot.mk CategoryTheory.FreeBicategory.Rel η

Instances For

@[simp]

theorem CategoryTheory.FreeBicategory.mk_vcomp {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} {f g h : a ⟶ b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ : CategoryTheory.FreeBicategory.Hom₂ g h) :

(η.vcomp θ).mk = CategoryTheory.CategoryStruct.comp η.mk θ.mk

@[simp]

theorem CategoryTheory.FreeBicategory.mk_whisker_left {B : Type u} [Quiver B] {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) {g h : b ⟶ c} (η : CategoryTheory.FreeBicategory.Hom₂ g h) :

(CategoryTheory.FreeBicategory.Hom₂.whisker_left f η).mk = CategoryTheory.Bicategory.whiskerLeft f η.mk

@[simp]

theorem CategoryTheory.FreeBicategory.mk_whisker_right {B : Type u} [Quiver B] {a b c : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} (η : CategoryTheory.FreeBicategory.Hom₂ f g) (h : b ⟶ c) :

(CategoryTheory.FreeBicategory.Hom₂.whisker_right h η).mk = CategoryTheory.Bicategory.whiskerRight η.mk h

theorem CategoryTheory.FreeBicategory.comp_def {B : Type u} [Quiver B] {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) :

CategoryTheory.FreeBicategory.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.FreeBicategory.mk_id {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :

Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.id f) = CategoryTheory.CategoryStruct.id f

@[simp]

theorem CategoryTheory.FreeBicategory.mk_associator_hom {B : Type u} [Quiver B] {a b c d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :

Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator f g h) = (CategoryTheory.Bicategory.associator f g h).hom

@[simp]

theorem CategoryTheory.FreeBicategory.mk_associator_inv {B : Type u} [Quiver B] {a b c d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :

Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h) = (CategoryTheory.Bicategory.associator f g h).inv

@[simp]

theorem CategoryTheory.FreeBicategory.mk_left_unitor_hom {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :

Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.left_unitor f) = (CategoryTheory.Bicategory.leftUnitor f).hom

@[simp]

theorem CategoryTheory.FreeBicategory.mk_left_unitor_inv {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :

Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv f) = (CategoryTheory.Bicategory.leftUnitor f).inv

@[simp]

theorem CategoryTheory.FreeBicategory.mk_right_unitor_hom {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :

Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.right_unitor f) = (CategoryTheory.Bicategory.rightUnitor f).hom

@[simp]

theorem CategoryTheory.FreeBicategory.mk_right_unitor_inv {B : Type u} [Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b) :

Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv f) = (CategoryTheory.Bicategory.rightUnitor f).inv

def CategoryTheory.FreeBicategory.of {B : Type u} [Quiver B] :

B ⥤q CategoryTheory.FreeBicategory B

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

@[simp]

theorem CategoryTheory.FreeBicategory.of_obj {B : Type u} [Quiver B] (a : B) :

CategoryTheory.FreeBicategory.of.obj a = id a

@[simp]

theorem CategoryTheory.FreeBicategory.of_map {B : Type u} [Quiver B] (x✝ x✝¹ : B) (f : x✝ ⟶ x✝¹) :

CategoryTheory.FreeBicategory.of.map f = CategoryTheory.FreeBicategory.Hom.of f

def CategoryTheory.FreeBicategory.liftHom {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C) {a b : CategoryTheory.FreeBicategory B} :

(a ⟶ b) → (F.obj a ⟶ F.obj b)

Auxiliary definition for lift.

Equations

CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.FreeBicategory.Hom.of f) = F.map f
CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.FreeBicategory.Hom.id x✝) = CategoryTheory.CategoryStruct.id (F.obj x✝)
CategoryTheory.FreeBicategory.liftHom F (f.comp g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.liftHom F f) (CategoryTheory.FreeBicategory.liftHom F g)

Instances For

@[simp]

theorem CategoryTheory.FreeBicategory.liftHom_id {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C) (a : CategoryTheory.FreeBicategory B) :

CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.id a) = CategoryTheory.CategoryStruct.id (F.obj a)

@[simp]

theorem CategoryTheory.FreeBicategory.liftHom_comp {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.CategoryStruct.{v₂, u₂} C] (F : B ⥤q C) {a b c : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c) :

CategoryTheory.FreeBicategory.liftHom F (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.liftHom F f) (CategoryTheory.FreeBicategory.liftHom F g)

def CategoryTheory.FreeBicategory.liftHom₂ {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} :

CategoryTheory.FreeBicategory.Hom₂ f g → (CategoryTheory.FreeBicategory.liftHom F f ⟶ CategoryTheory.FreeBicategory.liftHom F g)

Auxiliary definition for lift.

Instances For

theorem CategoryTheory.FreeBicategory.liftHom₂_congr {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} {η θ : CategoryTheory.FreeBicategory.Hom₂ f g} (H : CategoryTheory.FreeBicategory.Rel η θ) :

CategoryTheory.FreeBicategory.liftHom₂ F η = CategoryTheory.FreeBicategory.liftHom₂ F θ

def CategoryTheory.FreeBicategory.lift {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) :

CategoryTheory.Pseudofunctor (CategoryTheory.FreeBicategory B) 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

@[simp]

theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) {X✝ Y✝ : CategoryTheory.FreeBicategory B} (a✝ : X✝ ⟶ Y✝) :

(CategoryTheory.FreeBicategory.lift F).map a✝ = CategoryTheory.FreeBicategory.liftHom F a✝

@[simp]

theorem CategoryTheory.FreeBicategory.lift_mapComp {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) {a✝ b✝ c✝ : CategoryTheory.FreeBicategory B} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) :

(CategoryTheory.FreeBicategory.lift F).mapComp x✝ x✝¹ = CategoryTheory.Iso.refl ({ obj := F.obj, map := fun {X Y : CategoryTheory.FreeBicategory B} => CategoryTheory.FreeBicategory.liftHom F, map₂ := fun {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} => Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) ⋯, map₂_id := ⋯, map₂_comp := ⋯ }.map (CategoryTheory.CategoryStruct.comp x✝ x✝¹))

@[simp]

theorem CategoryTheory.FreeBicategory.lift_mapId {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) (x✝ : CategoryTheory.FreeBicategory B) :

(CategoryTheory.FreeBicategory.lift F).mapId x✝ = CategoryTheory.Iso.refl ({ obj := F.obj, map := fun {X Y : CategoryTheory.FreeBicategory B} => CategoryTheory.FreeBicategory.liftHom F, map₂ := fun {a b : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} => Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) ⋯, map₂_id := ⋯, map₂_comp := ⋯ }.map (CategoryTheory.CategoryStruct.id x✝))

@[simp]

theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) {a✝ b✝ : CategoryTheory.FreeBicategory B} {f✝ g✝ : a✝ ⟶ b✝} (a : Quot CategoryTheory.FreeBicategory.Rel) :

(CategoryTheory.FreeBicategory.lift F).map₂ a = Quot.lift (CategoryTheory.FreeBicategory.liftHom₂ F) ⋯ a

@[simp]

theorem CategoryTheory.FreeBicategory.lift_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj {B : Type u₁} [Quiver B] {C : Type u₂} [CategoryTheory.Bicategory C] (F : B ⥤q C) (a✝ : B) :

(CategoryTheory.FreeBicategory.lift F).obj a✝ = F.obj a✝