agda - 如何定义其定义隐含在键入中的类型？

Question

假设我想定义“类型的对角线”：

Σ[ x ∈ A ] Σ[ y ∈ A ] x ≡ y

在我看来，它应该是 A 中的平等类型。如果我尝试

data Diag (A : Set) : Σ[ x ∈ A ] Σ[ y ∈ A ] x ≡ y

它抱怨 Diag 是“定义但没有伴随定义”。关键是，它不应该已经定义了吗？

我怀疑在这种怀疑背后存在对类型在 Agda 中的工作方式的巨大误解。我来自 MLTT 的一门课程，在那里我可以得到类似的东西

其规范元素具有已知形状。

标签： agda