English
Two finite types α and β with the same cardinality are computably (up to truncation) equivalent: there is Trunc(α ≃ β).
Русский
Два конечных типа α, β с равной мощностью имеют вычислимую эквивалентность (с учётом трюка): существует Trunc(α ≃ β).
LaTeX
$$$\mathrm{Trunc}(\alpha \simeq \beta) \quad\text{whenever } \mathrm{card}\alpha = \mathrm{card}\beta.$$$
Lean4
/-- Two `Fintype`s with the same cardinality are (computably) in bijection.
See `Fintype.equivOfCardEq` for the noncomputable version,
and `Fintype.truncEquivFinOfCardEq` and `Fintype.equivFinOfCardEq` for
the specialization to `Fin`.
-/
def truncEquivOfCardEq [DecidableEq α] [DecidableEq β] (h : card α = card β) : Trunc (α ≃ β) :=
(truncEquivFinOfCardEq h).bind fun e => (truncEquivFin β).map fun e' => e.trans e'.symm
