如何通知 Agda 类型检查器两个类型确实相等？

Question

这是一个最小的（非）工作示例。

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)

我收到的错误如下：

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

但是，对于用户来说，很明显

A

和

combine A id

在给定上下文中具有相同的类型。 我不知道如何通知 agda 类型检查器这种情况。

我尝试过让

eq-2

依赖于

(combine A id) ≡ A

类型的东西，但这仍然不能解决问题。

我认为问题在于，仅仅因为这两种类型在命题上相等，并不意味着它们在定义上相等？ 如果是这种情况，有没有办法强制 agda 将命题相等解释为定义？

如有任何建议，我们将不胜感激。

Answer 1

一种选择是使用重写：

{-# 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

但这往往会掩盖太多，让事情变得难以推理。

另一种方法是使用某种形式的依赖相等：你有一个等式

eq : combine A id ≡ A

并且你想用

combine a id

over

a来识别

eq

。有关此想法的介绍，请参阅有关路径转换的注释。

使用Agda标准库，实现依赖相等的一种常见方法是使用

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

另一种方法是使用异构相等，它将类型的相等（由

≅-to-type-≡

见证）和类型的相等捆绑在一起（但是你需要

Type₃ A

被居住才能获得相等

combine A id ≡ A

） :

open import Relation.Binary.HeterogeneousEquality

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

如果您使用 Cubical Agda，您会想要使用类似

PathP

的东西。