Как определить тип, определение которого подразумевается в типизации?

Question

Скажем, я хочу определить «диагональ типа»:

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

На мой взгляд, это должен быть тип равенства в A. Если я попытаюсь с

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

Он жалуется, что Diag "определен, но не сопровождается определением" .Дело в том, разве это не должно быть уже определено?

Я подозреваю, что за этим сомнением существует большое недопонимание того, как типы работают в Agda.Я пришел из курса в MLTT, и там я могу получить что-то вроде

, чьи канонические элементы имеют известную форму.