`Refl` Ding in der Konstruktionsrechnung?

In Sprachen wieAgda, Idris, oderHaskell mit Typerweiterungen gibt es ein= Typ Art wie die folgenden

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

a :~: b bedeutet, dassa undb sind gleich

Kann ein solcher Typ im @ definiert werdKalkül von Konstruktionen oder Morte (welche Programmiersprache basiert auf der Konstruktionsrechnung)?