Em idiomas comoAgda, IdrisouHaskell com extensões de tipo, existe um= tipo como o seguinte

data a :~: b where
  Refl :: a :~: a

a :~: b significa quea eb são os mesmos.

Esse tipo pode ser definido nocálculo de construções ouMorte (qual é a linguagem de programação baseada no cálculo da construção)?