Theorems · Theorem · category theory

FintypeCat.uSwitchEquiv_naturality

∀ {X Y : FintypeCat} (f : X ⟶ Y) (x : (FintypeCat.uSwitch.obj X).obj),
  (CategoryTheory.ConcreteCategory.hom f) (X.uSwitchEquiv x) =
    Y.uSwitchEquiv ((CategoryTheory.ConcreteCategory.hom (FintypeCat.uSwitch.map f)) x)

Defined in

Mathlib.CategoryTheory.FintypeCat

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound