∀ {α : Type u_6} {β : Type u_7} [inst : Min α] [inst_1 : Min β] [inst_2 : SizeOf α] [inst_3 : SizeOf β] (toFun : α → β)
  (map_inf' : ∀ (a b : α), toFun (a ⊓ b) = toFun a ⊓ toFun b), sizeOf { toFun := toFun, map_inf' := map_inf' } = 1