如何编写此coq代码的agda等效代码？

Question

我想在agda中编写给定的coq代码。

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 in Agda相当于Coq中的Inductive：它引入了一种归纳定义的新类型。

的Definition在阿格达等效简直是要界定一个东西定义公式：

postulate R : Set 

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