title: `Refl` thing in Calculus of Constructions?
body: <p>In languages such as <code>Agda</code>, <code>Idris</code>, or <code>Haskell</code> with type extensions, there is a <code>=</code> type sort of like the following</p>
  
  <pre><code>data a :~: b where
    Refl :: a :~: a
  </code></pre>
  
  <p><code>a :~: b</code> means that <code>a</code> and <code>b</code> are the same.</p>
  
  <p>Can such a type be defined in the <a href="https://en.wikipedia.org/wiki/Calculus_of_constructions" rel="noreferrer">calculus of constructions</a> or <a href="https://github.com/Gabriel439/Haskell-Morte-Library" rel="noreferrer">Morte</a> (which is programming language based on the calculus of construction)?</p>