V minulém díle jsme si řekli, že v Idrisu jsou kromě „běžných“ typů také typy rovnostní, jejichž (generickou) definici si můžeme představit zhruba takto: /---pre data (=) : a → b → Type where Refl : x = x \--- Konstruktor je nanejvýš jeden, a to pouze v případě, že se oba argumenty shodují. To dává smysl, připomeňte si, že typy odpovídají logickým výrokům, takže existence konstruktoru znamená, že výrok platí.