Как правильно определить запись с параметрами в Agda? - PullRequest
Новая
       67

Как правильно определить запись с параметрами в Agda?

0 голосов
/ 10 марта 2020

Я использую Agda 2.5.3 и HoTT Agda для изучения теории гомотопических типов. Я определил простой S¹: 

data S¹ : Type₀ where
  base : S¹

postulate
  loop : base == base

и теперь я пытаюсь определить тип записи для функции, которая действует как принцип рекурсии круга для типа A: 

record is-S¹-rec {i} {A : Set i} (base* : A) (loop* : base* == base*) : Set i where
  field
    f : S¹ → A
    f-base : f base == base*
    f-loop : apd f loop == loop* [ Path ↓ f-base ]

Но я получаю эту ошибку: 

(_A_22 base* loop* f f-base → Set (_i_20 base* loop* f f-base)) !=<
Set (_i_20 base* loop* f f-base) of type
Set (lsucc (_i_20 base* loop* f f-base))
when checking that the expression Path has type
_A_22 base* loop* f f-base → Type (_i_20 base* loop* f f-base)

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

...