In languages such as Agda
, Idris
, or Haskell
with type extensions, there is a =
type sort of like the following
data a :~: b where
Refl :: a :~: a
a :~: b
means that a
and b
are the same.
Can such a type be defined in the calculus of constructions or Morte (which is programming language based on the calculus of construction)?
The standard Church-encoding of
a :~: b
in CoC is:Refl
beingThe above formulates equality between types. For equality between terms, the
:~:
relation must take an additional argumentt :: *
, wherea b :: t
.