uSwitchEquivalence — Mathlib

Lean4

/-- `uSwitch.{u, v}` is an equivalence of categories with quasi-inverse `uSwitch.{v, u}`. -/
noncomputable def uSwitchEquivalence : FintypeCat.{u} ≌ FintypeCat.{v}
    where
  functor := uSwitch
  inverse := uSwitch
  unitIso :=
    NatIso.ofComponents (fun X ↦ (equivEquivIso <| (uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv).symm) <| by
      simp [uSwitch_map_uSwitch_map]
  counitIso :=
    NatIso.ofComponents (fun X ↦ equivEquivIso <| (uSwitch.obj X).uSwitchEquiv.trans X.uSwitchEquiv) <| by
      simp [uSwitch_map_uSwitch_map]
  functor_unitIso_comp
    X := by
    ext x
    simp [← uSwitchEquiv_naturality]

Похожие утверждения