How to Notify the Agda Type-Checker that two Types are Indeed Equal?

Here is a minimum (not-)working example.

infix 4 _≡_
data _≡_ {a} {A : Set a} (x : A) : A → Set a where
    refl : x ≡ x
{-# BUILTIN EQUALITY _≡_  #-}

data Type₁ : Set where
    id : Type₁
    non-id : Type₁

data Type₂ : Set where
    combine : Type₂ → Type₁ → Type₂

data Type₃ : Type₂ → Set where
    combine : {a : Type₂} → (Type₃ a) → (b : Type₁) → (Type₃ (combine a b))

postulate
    eq : {A : Type₂} → ((combine A id) ≡ A)
    eq-2 : {A : Type₂} → {a : Type₃ A} → ((combine a id) ≡ a)

The error I receive is as follows:

A != combine A id of type Type₂
when checking that the expression a has type Type₃ (combine A id)

However, it is obvious to the user that A and combine A id have the same types in the given context. I don't know how to inform the agda type-checker that this is the case.

I have tried making eq-2 depend on something of type (combine A id) ≡ A, but this still doesn't solve the problem.

I think the problem is that just because these two types are propositionally equal, it doesn't imply that they are definitionally equal? If this is the case, is there a way to force agda to interpret propositional equality as definitional?

Any advice would be greatly appreciated.

Solution

One option is to use rewriting:

{-# OPTIONS --rewriting #-}
open import Agda.Builtin.Equality
open import Agda.Builtin.Equality.Rewrite

postulate
    eq : {A : Type₂} → combine A id ≡ A

{-# REWRITE eq #-}

postulate
    eq-2 : {A : Type₂} → {a : Type₃ A} → combine a id ≡ a

But this tends to sweep too much under the rug and make things hard to reason about.

Another approach is to use some form of dependent equality: you have an equality eq : combine A id ≡ A and you want to identify combine a id : combine A id with a : A over eq. For an introduction to this idea, see this note on pathovers.

Using the Agda standard library, one common way to implement dependent equality is to use subst:

open import Relation.Binary.PropositionalEquality

postulate
    eq : {A : Type₂} → combine A id ≡ A
    eq-2 : {A : Type₂} → {a : Type₃ A} → subst Type₃ eq (combine a id) ≡ a

Another is to use heterogeneous equality, which bundles together an equality of types (witnessed by ≅-to-type-≡) and an equality over that (but then you need Type₃ A to be inhabited in order to get an equality combine A id ≡ A):

open import Relation.Binary.HeterogeneousEquality

postulate
    eq-2 : {A : Type₂} → {a : Type₃ A} → combine a id ≅ a

If you use Cubical Agda, you'll want to use something like PathP.