Skip to main content

OrderDualIso

structure OrderDualIso[A: PartialOrder, B: PartialOrder] {
    map: A -> B
    inv: B -> A
} constraint {
    is_order_dual_iso_pair(map, inv)
}

An order-dual isomorphism with explicit inverse data.

GitHub

inv​

OrderDualIso.inv: (OrderDualIso[A, B], B) -> A

The inverse order-reversing map.

map​

OrderDualIso.map: (OrderDualIso[A, B], A) -> B

The order-reversing map.