Theorems · Inductive type · category theory

CategoryTheory.HalfBraiding

{C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → C → Type (max u₁ v₁)

A half-braiding on X : C is a family of isomorphisms X ⊗ U ≅ U ⊗ X, monoidally natural in U : C. Thinking of C as a 2-category with a single 0-morphism, these are the same as natural transformations (in the pseudo- sense) of the identity 2-functor on C, which send the unique 0-morphism to X.

Defined in

Mathlib.CategoryTheory.Monoidal.Center

Cited by

62 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategory