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](https://en.wikipedia.org/wiki/Calculus_of_constructions) or [Morte](https://github.com/Gabriel439/Haskell-Morte-Library) (which is programming language based on the calculus of construction)?