English
A type-level equivalence e: α ≃ β induces an equivalence of the discrete categories Discrete α ≌ Discrete β.
Русский
Эквивалентость типа e: α ≃ β порождает эквивалентность между дискретными категориями Discrete α и Discrete β.
LaTeX
$$$\\text{equivalence } (\\alpha,\\beta) \\Rightarrow \\mathrm{Discrete}(\\alpha) \\simeq \\mathrm{Discrete}(\\beta)$$$
Lean4
/-- We can convert an equivalence of `discrete` categories to a type-level `Equiv`. -/
@[simps]
def equivOfEquivalence {α : Type u₁} {β : Type u₂} (h : Discrete α ≌ Discrete β) : α ≃ β
where
toFun := Discrete.as ∘ h.functor.obj ∘ Discrete.mk
invFun := Discrete.as ∘ h.inverse.obj ∘ Discrete.mk
left_inv a := by simpa using eq_of_hom (h.unitIso.app (Discrete.mk a)).2
right_inv a := by simpa using eq_of_hom (h.counitIso.app (Discrete.mk a)).1
