Should I define several classes for equivalent structures?

Stream: new members

[Victor Porton]

When there is several ways to define equivalent algebraic structures (in the example below PosetFilter and PosetFilter2), should I define several classes, like the following:

structure PosetFilterBase{α: Type*}(U: PartialOrder α) where
  elements: Set α
  non_empty: Set.Nonempty elements
  cap_elements {x y: α} : x ∈ elements → y ∈ elements → ∃ z ∈ elements, (z ≤ x ∧ z ≤ y)

structure PosetFilter{α: Type*}(U: PartialOrder α) extends PosetFilterBase U, UpperSet α where
  carrier_eq_elements : carrier = elements

structure PosetFilter2{α: Type*}(U: PartialOrder α) where
  elements: Set α
  non_empty: Set.Nonempty elements
  cap_elements {x y: α} : x ∈ elements ∧ y ∈ elements ↔ ∃ z ∈ elements, (z ≤ x ∧ z ≤ y)

or should I use some other ways (simply, conversion functions?) to describe such situations? Could you describe the pattern (if any) in more details?

Also, how to name them? (like PosetFilter2 or how?)

[Victor Porton]

Also, should I define coercions between such equivalent structures?

[Notification Bot]

This topic was moved here from #lean4 > Should I define several classes for equivalent structures? by Michael Rothgang.