Why doesn't this dual poset definition don't type check

Question

I created the following poset definition, the dual definition doesn't type check for antisymmetry. I am not sure how to make it work, any suggestions?

structure Poset {α : Type} (leq : α → (α → Prop)) :=  mkPoset :: 
    (reflexive: (∀x : α, (leq x x))) 
    (antisymmetric : (∀x y : α, (leq x y) → (leq y x) → x = y))
    (transitive : (∀x y z: α, (leq x y) → (leq y z) → (leq x z)))

section Poset
    parameter α : Type
    parameter leq : α → α → Prop
    parameter poset: (Poset leq)

    def geq (x: α)(y: α) := leq y x


    def dual : Poset geq := Poset.mkPoset poset.reflexive (λx y: α, poset.antisymmetric y x) (λ x y z: α, poset.transitive z y x)
end Poset

Answer 1

Let's take a look at the error message:

term
  λ (x y : α), poset.antisymmetric y x
has type
  ∀ (x y : α), leq y x → leq x y → y = x
but is expected to have type
  ∀ (x y : α), geq x y → geq y x → x = y

While the assumptions are definitionally equal, the conclusion is not. You have to apply eq.symm at the right location.

def dual : Poset geq :=
{ reflexive := poset.reflexive,
  antisymmetric := λ x y h₁ h₂, eq.symm (poset.antisymmetric y x h₁ h₂),
  -- note, this is not quite correct yet either
  transitive := λ x y z, poset.transitive z y x }