PROSAGA码农传奇-精益-如何在精益中定义部分有序集？

<div class =“post-text”itemprop =“text”>
  
    我不是精益用户，但这是我在Agda中定义它的方式。它可能无法直接翻译 - 类型理论有很多种 - 但它至少应该是一个指针！
  
  
    我们将使用二元逻辑关系，这是这种同义词的居民：
  
   <pre>
 <code>
 Rel : Set -> Set1
Rel A = A -> A -> Set

</code>
 </pre>
  
    我们需要命题平等：
  
   <pre>
 <code>
 data _==_ {A : Set} (x : A) : A -> Set where
 refl : x == x

</code>
 </pre>
  
    人们可以说逻辑关系意味着什么
    <a href="https://en.wikipedia.org/wiki/Reflexive_relation" rel="nofollow noreferrer">
      反思
    </A>
    ，
    <a href="https://en.wikipedia.org/wiki/Antisymmetric_relation" rel="nofollow noreferrer">
      反对称
    </A>
    ，和
    <a href="https://en.wikipedia.org/wiki/Transitive_relation" rel="nofollow noreferrer">
      及物
    </A>
    。
  
   <pre>
 <code>
 Refl : {A : Set} -> Rel A -> Set
Refl {A} _~_ = {x : A} -> x ~ x

Antisym : {A : Set} -> Rel A -> Set
Antisym {A} _~_ = {x y : A} -> x ~ y -> y ~ x -> x == y

Trans : {A : Set} -> Rel A -> Set
Trans {A} _~_ = {x y z : A} -> x ~ y -> y ~ z -> x ~ z

</code>
 </pre>
  
    要成为一个部分订单，它必须全部三个。
  
   <pre>
 <code>
 record IsPartialOrder {A : Set} (_<=_ : Rel A) : Set where
 field
 reflexive : Refl _<=_
 antisymmetric : Antisym _<=_
 transitive : Trans _<=_

</code>
 </pre>
  
    一个
    <a href="https://en.wikipedia.org/wiki/Partially_ordered_set" rel="nofollow noreferrer">
      偏序集
    </A>
     只是一个配备部分排序关系的集合。
  
   <pre>
 <code>
 record Poset : Set1 where
 field
 carrier : Set
 _<=_ : Rel carrier
 isPartialOrder : IsPartialOrder _<=_

</code>
 </pre>
  <HR />
  
    为了记录（哈哈），这里是如何
    <a href="https://en.wikipedia.org/wiki/Setoid" rel="nofollow noreferrer">
      setoid
    </A>
     本教程中的示例转换为Agda：
  
   <pre>
 <code>
 Sym : {A : Set} -> Rel A -> Set
Sym {A} _~_ = {x y : A} -> x ~ y -> y ~ x

record IsEquivalence {A : Set} (_~_ : Rel A) : Set where
  field
    reflexive : Refl _~_
    symmetric : Sym _~_
    transitive : Trans _~_

record Setoid : Set1 where
  field
    carrier : Set
    _~_ : Rel carrier
    isEquivalence : IsEquivalence _~_

</code>
 </pre>
  <HR />
  
    的
      更新
    </强>
    ：我安装了Lean，犯了很多语法错误，并最终达到了这个（可能不是惯用，但直截了当）的翻译。功能成为
     <code>
 definition
 </code>
    s和
     <code>
 record
 </code>
    成了
     <code>
 structure
 </code>
    秒。
  
   <pre>
 <code>
 definition Rel (A : Type) : Type := A -> A -> Prop

definition IsPartialOrder {A : Type}(P : Rel A) :=
  reflexive P �� anti_symmetric P �� transitive P

structure Poset :=
  (A : Type)
  (P : Rel A)
  (ispo : IsPartialOrder P)

</code>
 </pre>
  
    我正在使用
    <a href="https://github.com/leanprover/lean/blob/master/library/init/relation.lean" rel="nofollow noreferrer">
      内置版本
    </A>
     我在上面的Agda中定义的自反性（等）的定义。我也注意到精益似乎很高兴让我省略宇宙水平
     <code>
 Type
 </code>
     在返回类型中
     <code>
 Rel
 </code>
     上面，这是一个很好的接触。
  
</DIV>