title: How to define arbitrary partial order relation and prove its properties?
body: <p>I have a simple data type with all nullary constructors and wish to define a partial order for it, including a <code>Relation.Binary.IsPartialOrder _≡_</code>.</p>
  
  <p>My use case: the type is the type of sorts in an abstract syntax tree (statement, expression, literal, item), and i want a constructor of the AST which effectively upcasts a term (item ≤ statement, expression ≤ statement, literal ≤ expression).</p>
  
  <pre><code>data Sort : Set where stmt expr item lit : Sort
  </code></pre>
  
  <p>So far i have this:</p>
  
  <pre><code>data _≤_ : Rel Sort lzero where
      refl : {a : Sort} → a ≤ a
      trans : {a b c : Sort} → a ≤ b → b ≤ c → a ≤ c
      expr≤stmt : expr ≤ stmt
      item≤stmt : item ≤ stmt
      lit≤expr : lit ≤ expr
  </code></pre>
  
  <p>I can define <code>isPreorder</code> but have no idea how to define <code>antisym</code>:</p>
  
  <pre><code>open import Agda.Primitive
  open import Data.Empty using (⊥)
  open import Data.Unit using (⊤)
  open import Relation.Binary
  open import Relation.Binary.PropositionalEquality using (_≡_)
  import Relation.Binary.PropositionalEquality as PropEq
  
  module Core.Sort where
  
  data Sort : Set where
      stmt expr item lit : Sort
  
  data _≤_ : Rel Sort lzero where
      refl : {a : Sort} → a ≤ a
      trans : {a b c : Sort} → a ≤ b → b ≤ c → a ≤ c
      lit≤expr  : lit  ≤ expr
      expr≤stmt : expr ≤ stmt
      item≤stmt : item ≤ stmt
  
  ≤-antisymmetric : Antisymmetric _≡_ _≤_
  ≤-antisymmetric =
      λ { refl _ → PropEq.refl;
          _ refl → PropEq.refl;
          (trans refl x≤y) y≤x → ≤-antisymmetric x≤y y≤x;
          (trans x≤y refl) y≤x → ≤-antisymmetric x≤y y≤x;
          x≤y (trans refl y≤x) → ≤-antisymmetric x≤y y≤x;
          x≤y (trans y≤x refl) → ≤-antisymmetric x≤y y≤x;
          x≤z (trans z≤y (trans y≤w w≤x)) → _ }
  </code></pre>
  
  <p>I'm not sure what to do in the last clause (and all further clauses like it), and in any case this is cumbersome.</p>
  
  <p>Am i missing a more convenient method to define an arbitrary partial order?</p>