agda: How do I tell the type system that two types are equal?

Say I have type dependent on Nat

data MyType : (i : ℕ) → Set where
  cons : (i : ℕ) → MyType i

and a function:

combine : {i₁ i₂ : ℕ} → MyType i₁ → MyType i₂ → MyType (i₁ ⊔ i₂)

Now I'm trying to write a function:

create-combined : (i : ℕ) → MyType i
create-combined i = combine {i} {i} (cons i) (cons i)

Unfortunately, I get the error message:

i ⊔ i != i of type ℕ
when checking that the inferred type of an application
  MyType (i ⊔ i)
matches the expected type
  MyType i

I know I can prove i ⊔ i ≡ i, but I don't know how to give that proof to the type system in order to get this to resolve.

How do I get this to compile?

Solution

You can use subst from Relation.Binary.PropositionalEquality.

You give it:

the proof that i ⊔ i ≡ i
the dependent type that should be transformed with the proof, in your case MyType
the term to be transformed, in your case combine {i} {i} (cons i) (cons i)

Or you can use the rewrite keyword as well on your proof, which is usually to be preferred.

Here is an (artificial) example of both possibilities applied on vector concatenation:

module ConsVec where

open import Data.Vec
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality

_++₁_ : ∀ {a} {A : Set a} {m n} → Vec A m → Vec A n → Vec A (n + m)
_++₁_ {m = m} {n} v₁ v₂ = subst (Vec _) (+-comm m n) (v₁ ++ v₂)

_++₂_ : ∀ {a} {A : Set a} {m n} → Vec A m → Vec A n → Vec A (n + m)
_++₂_ {m = m} {n} v₁ v₂ rewrite sym (+-comm m n) = v₁ ++ v₂