Понимание проблем вывода типов в agda при проверке законов применения функций basi c

Question

Я пытаюсь доказать закон идентичности для приложения функции. Я выделяю желтым цветом предполагаемую функцию идентификации, apfId, ниже. Не понимаю, разве _≡_ {A} не имеет типа A → A → Set? Есть ли простой способ проверить тип выражения в Agda, например: t в ghci?

———— Error —————————————————————————————————————————————————
/home/wmacmil/agda2020/agda/MLTT/Id.agda:217,49-55
Set₁ != Set
when checking that the expression _≡_ {A} has type A → A → Set

Мы очень ценим любые предложения.

data _≡_ {A : Set} (a : A) : A → Set where
  r : a ≡ a

infix 20 _≡_

J : {A : Set}
    → (D : (x y : A) → (x ≡ y) →  Set)
    -- → (d : (a : A) → (D a a r ))
    → ((a : A) → (D a a r ))
    → (x y : A)
    → (p : x ≡ y)
    ------------------------------------
    → D x y p
J D d x .x r = d x


-- ap\_
apf : {A B : Set} → {x y : A} → (f : A → B) → (x ≡ y) → f x ≡ f y
apf {A} {B} {x} {y} f p = J D d x y p
  where
    D : (x y : A) → x ≡ y → Set
    D x y p = {f : A → B} → f x ≡ f y
    d : (x : A) → D x x r
    d = λ x → r 

apfId : {A : Set} {x y : A} (p : x ≡ y) → (apf (_≡_ {A}) p) ≡ p -- it highlights yellow at the _≡_

Answer 1

Я неверно истолковал функцию id_A в книге HoTT как тип идентичности A (обычно обозначаемый Id_A xx), а не функцию идентификации idA: A -> A.