CategoryTheory.FreeBicategory.normalizeAux_congr
theorem CategoryTheory.FreeBicategory.normalizeAux_congr :
∀ {B : Type u} [inst : Quiver B] {a b c : B} (p : Quiver.Path a b) {f g : CategoryTheory.FreeBicategory.Hom b c},
(f ⟶ g) → CategoryTheory.FreeBicategory.normalizeAux p f = CategoryTheory.FreeBicategory.normalizeAux p g
This theorem states that in the free bicategory, given a 2-morphism between two 1-morphisms `f` and `g` from objects `b` to `c`, the result of applying the function `normalizeAux` to `p` and `f` is equal to the result of applying `normalizeAux` to `p` and `g`. Here, `p` represents a path in the underlying quiver from object `a` to `b`, `B` is a type equipped with a quiver structure, and the free bicategory is constructed from this quiver.
More concisely: In the free bicategory constructed from a quiver, the normalization of a path with respect to a 1-morphism `f` from object `b` to `c` is equal to the normalization of the same path with respect to another 1-morphism `g` if and only if `f` and `g` are equivalent as 1-morphisms.
|
CategoryTheory.FreeBicategory.normalize_naturality
theorem CategoryTheory.FreeBicategory.normalize_naturality :
∀ {B : Type u} [inst : Quiver B] {a b c : B} (p : Quiver.Path a b) {f g : CategoryTheory.FreeBicategory.Hom b c}
(η : f ⟶ g),
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Bicategory.whiskerLeft ((CategoryTheory.FreeBicategory.preinclusion B).map { as := p }) η)
(CategoryTheory.FreeBicategory.normalizeIso p g).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.normalizeIso p f).hom
((CategoryTheory.FreeBicategory.preinclusion B).map₂ (CategoryTheory.eqToHom ⋯))
This theorem, `CategoryTheory.FreeBicategory.normalize_naturality`, states that in any quiver `B` (a category where each hom-set is a singleton set, so morphisms are basically just arrows) and for any three objects `a`, `b`, and `c` in `B`, and for any path `p` from `a` to `b`, and any two morphisms `f` and `g` from `b` to `c`, and a morphism `η` from `f` to `g`, the 2-isomorphism `normalizeIso p f` is natural in `f`. That is, if we first whisker (post-compose) the morphism `η` with the pre-inclusion of the path `p` into `B` and then compose the result with the hom of `normalizeIso p g`, we get the same result as if we first take the hom of `normalizeIso p f` and then compose it with the pre-inclusion of the equality morphism from `f` to `g` into `B`.
More concisely: In any quiver, for any path, morphisms, and 2-isomorphism, whiskering the 2-isomorphism with the morphism pre-inclusion of the path and then composing with the hom of the morphism is equal to taking the hom of the 2-isomorphism and then composing with the morphism equality.
|
CategoryTheory.FreeBicategory.preinclusion_map₂
theorem CategoryTheory.FreeBicategory.preinclusion_map₂ :
∀ {B : Type u} [inst : Quiver B] {a b : B} (f g : CategoryTheory.Discrete (Quiver.Path a b)) (η : f ⟶ g),
(CategoryTheory.FreeBicategory.preinclusion B).map₂ η = CategoryTheory.eqToHom ⋯
The theorem `CategoryTheory.FreeBicategory.preinclusion_map₂` states that for any type `B` equipped with a `Quiver` structure, and for any two objects `a` and `b` in `B`, given two discrete paths `f` and `g` from `a` to `b` in the discrete quiver and a morphism `η` from `f` to `g`, applying the `map₂` function of the `preinclusion` of the free bicategory of `B` to `η` will yield the same result as applying the `eqToHom` function to a certain equality. The `eqToHom` function is used to turn an equality into a morphism in a category, avoiding potential complications from dependent type theory.
More concisely: For any type `B` with a `Quiver` structure, given two objects `a` and `b`, discrete paths `f` and `g` from `a` to `b`, and a morphism `η` from `f` to `g`, `preinclusion_map₂ η = eqToHom (ap _ _ η)` in the free bicategory of `B`.
|