Как это записать в agda?

Question

Я хотел реализовать это утверждение в agda;

A dedekind cut is a pair (L, U) of mere predicates L : Q -> Set and R : Q -> Set which is 
1) inhibited : exists (q : Q) . L(q)^exists (r : Q) . U(r) 

Я попытался таким образом,

record cut : Set where 
    field 
     L : Q -> Set 
     R : Q -> Set 
     inhibited : exists (q : Q) . L(q)^exists (r : Q) . U(r) 

, но это не работает. Я хочу написать это, и я поражен, пожалуйста, помогите. А также то, что разница между 1)data R : Set and record R : Set and 2) data R : Set and data R : Q -> Set

Answer 1

Я не знаю об определении всего Дедекинда вырезать, хотя я нашел свое определение на странице 369 Гомотопического теории Типа: однолистных Основа математики.

Вот синтаксис для определения того, что вы задавали в своем вопросе, в двух формах: один с использованием стандартной библиотеки и один расширенный, чтобы показать, что он делает.

open import Data.Product using (∃) 

record Cut (Q : Set) : Set₁ where 
    field 
    L U : Q → Set -- The two predicates 
    L-inhabited : ∃ L 
    U-inhabited : ∃ U 

Если вручную расширить определение ∃ (существует) мы имеем:

record Cut′ (Q : Set) : Set₁ where 
    field 
    L U : Q → Set -- The two predicates 
    q r : Q  -- Witnesses 
    Lq : L q  -- Witness satisfies predicate 
    Ur : U r  -- Witness satisfies predicate 

Обратите внимание, что запись имеет тип Set₁ в связи с типами полей L и U.

Что касается вашего вопроса о записях и индуктивно определенных типах данных, есть много различий. Возможно, вы захотите начать с вики и задавать более конкретные вопросы, если вы застряли где-нибудь: Data, Records