mathlib3 documentation


The category of types is a symmetric monoidal category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

theorem category_theory.braiding_hom_apply {X Y : Type u} {x : X} {y : Y} :
(β_ X Y).hom (x, y) = (y, x)
theorem category_theory.braiding_inv_apply {X Y : Type u} {x : X} {y : Y} :
(β_ X Y).inv (y, x) = (x, y)