∀ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst_1 : SupSet β],
  Function.LeftInverse (fun f => { toFun := ⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual, map_sSup' := ⋯ }) fun f =>
    { toFun := ⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual, map_sInf' := ⋯ }