title: agda: How do I tell the type system that two types are equal?
body: <p>Say I have type dependent on Nat</p>
  <pre><code>data MyType : (i : ℕ) → Set where
    cons : (i : ℕ) → MyType i
  </code></pre>
  <p>and a function:</p>
  <pre><code>combine : {i₁ i₂ : ℕ} → MyType i₁ → MyType i₂ → MyType (i₁ ⊔ i₂)
  </code></pre>
  <p>Now I'm trying to write a function:</p>
  <pre><code>create-combined : (i : ℕ) → MyType i
  create-combined i = combine {i} {i} (cons i) (cons i)
  </code></pre>
  <p>Unfortunately, I get the error message:</p>
  <pre><code>i ⊔ i != i of type ℕ
  when checking that the inferred type of an application
    MyType (i ⊔ i)
  matches the expected type
    MyType i
  </code></pre>
  <p>I know I can prove <code>i ⊔ i ≡ i</code>, but I don't know how to give that proof to the type system in order to get this to resolve.</p>
  <p>How do I get this to compile?</p>