Как написать эквивалентный код agda этого кода coq?

Question

Я хочу написать данный код coq в agda.

Definition included (D1 D2:R -> Prop) : Prop := forall x:R, D1 x -> D2 x. 

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

data included (D1 D2 : R -> Set) : Set where 
     forall x : R D1 x -> D2 x 

Я знаю, что проблема во второй линии, но, как это исправить. Нужно ли определять конструктор? И как я это сделаю?

помогите пожалуйста.

Answer 1

data в Агда это эквивалент Inductive в Coq: он вводит новый тип, определяемый индуктивно.

Эквивалент Definition в Agda просто определяющее уравнение для, что вы хотите, чтобы определить:

postulate R : Set 

included : (_ _ : R → Set) → Set 
included D1 D2 = ∀ x → D1 x → D2 x