# Tutorial: setoids A _setoid_ is a type equipped with an equivalence relation F : Nat
F = 0