English
An equivalence between the discrete categories Discrete α and Discrete β yields a type-level equivalence α ≃ β.
Русский
Эквивалентность между дискретными категориями Discrete α и Discrete β даёт эквивалентность типов α ≃ β.
LaTeX
$$$\\text{Discrete equivalence } h: \\mathrm{Discrete}(\\alpha) \\simeq \\mathrm{Discrete}(\\beta) \\Rightarrow \\alpha \\simeq \\beta$$$
Lean4
/-- We can promote a type-level `Equiv` to
an equivalence between the corresponding `discrete` categories.
-/
@[simps]
def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ Discrete J
where
functor := Discrete.functor (Discrete.mk ∘ (e : I → J))
inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I))
unitIso := Discrete.natIso fun i => eqToIso (by simp)
counitIso := Discrete.natIso fun j => eqToIso (by simp)
