CategoryTheory.OplaxNatTrans.ext
theorem CategoryTheory.OplaxNatTrans.ext :
∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
{F G : CategoryTheory.OplaxFunctor B C} {α β : F ⟶ G} {m n : α ⟶ β}, (∀ (b : B), m.app b = n.app b) → m = n
This theorem states that in the context of bicategories and oplax functors, if two natural transformations `α` and `β` between oplax functors `F` and `G` have two morphisms `m` and `n` from `α` to `β` such that the application of `m` and `n` to any object `b` in the bicategory `B` gives the same result, then `m` and `n` are the same morphism. This theorem is a statement about the uniqueness of morphisms between natural transformations in the setting of oplax functors. The theorem holds for any types `B` and `C` that form bicategories.
More concisely: In the context of bicategories and oplax functors, if two natural transformations between them have morphisms making all component maps equal, then those morphisms are equal.
|
CategoryTheory.OplaxNatTrans.Modification.ext
theorem CategoryTheory.OplaxNatTrans.Modification.ext :
∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
{F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (x y : CategoryTheory.OplaxNatTrans.Modification η θ),
x.app = y.app → x = y
This theorem states that, given two types `B` and `C` each equipped with a structure of bicategory, two oplax functors `F` and `G` from `B` to `C`, and two oplax natural transformations `η` and `θ` from `F` to `G`; if we have two modifications `x` and `y` between `η` and `θ`, and the application of these modifications `x.app` and `y.app` are the same, then the modifications `x` and `y` are themselves the same. This theorem holds in the context of category theory and oplax natural transformations.
More concisely: If two modifications between two oplax natural transformations between bicategory structures with the same domain and codomain have equal application, then they are equal.
|