Sebas demonstration

// (τ₁ -> τ₂) ⊓ (π₁ -> π₂) ≡ (τ₁ ⊔ π₁) -> (τ₂ ⊓ π₂)
(#A -> {a: top}) & (#B -> {b: top}) <: (#A | #B) -> ({a: top} & {b: top})
(#A | #B) -> ({a: top} & {b: top}) <: (#A -> {a: top}) & (#B -> {b: top})

// {a: τ} ⊔ {b: π} ≡ ⊤
{a: bot} | {b: bot} <: top
top <: {a: bot} | {b: bot}

// {a: τ} ⊔ (π₁ -> π₂) ≡ ⊤
{a: bot} | (top -> bot) <: top
top <: {a: bot} | (top -> bot)

// #T ⊓ #S ≡ ⊥
#T & #S <: bot
bot <: #T & #S

// α ↦ Int
//   |-
// α <: Int
'a == #Int
  |-
'a <: #Int

bot -> top <: top
{a: top} <: top
{b: top} <: top
(bot -> top) & {a: top} <: bot -> top
(bot -> top) & {a: top} & {b: top} <: bot -> top
(bot -> top) & {a: top} <: {a: top}
(bot -> top) & {a: top} & {b: top} <: {a: top}
{a: top} & {b: top} <: {a: top}
(bot -> top) & {a: top} & {b: top} <: {b: top}
{a: top} & {b: top} <: {b: top}

// ¬{a: τ} <: {b: π}
~{a: top} <: {b: top}

// (#Some ⊓ {value: α} ⊔ β ⊓ ¬#Some ⊓ #Obj) ⊓ ¬#Some <: β ⊓ ¬#Some ⊓ #Obj
// β ⊓ ¬#Some ⊓ #Obj <: (#Some ⊓ {value: α} ⊔ β ⊓ ¬#Some ⊓ #Obj) ⊓ ¬#Some
'a == top
'b == top
  |-
(#Some & {value: 'a} | 'b & ~#Some & #) & ~#Some <: 'b & ~#Some & #
'b & ~#Some & # <: (#Some & {value: 'a} | 'b & ~#Some & #) & ~#Some

// {a₁: τ₁} ⊓ {a₃: τ₃} ⊓ {a₄: τ₄} <: {a₁: τ₁} ⊓ {a₂: τ₂} ⊓ {a₃: τ₃} ⊓ {a₄: τ₄} ⊔ ¬{a₂: ⊥}
// {a₁: τ₁} ⊓ {a₂: τ₂} ⊓ {a₃: τ₃} ⊓ {a₄: τ₄} ⊔ ¬{a₂: ⊥} <: {a₁: τ₁} ⊓ {a₃: τ₃} ⊓ {a₄: τ₄}
{a1: #A1} & {a3: #A3} & {a4: #A4} <: {a1: #A1} & {a2: #A2} & {a3: #A3} & {a4: #A4} | ~{a2: bot}
{a1: #A1} & {a2: #A2} & {a3: #A3} & {a4: #A4} | ~{a2: bot} <: {a1: #A1} & {a3: #A3} & {a4: #A4}

// ⊤ <: {a: τ₁} ⊔ {b: τ₂}
top <: {a: bot} | {b: bot}

// ¬{a: τ₁} <: {b: τ₂}
~{a: bot} <: {b: bot}

// {a₁: τ₁} ⊓ {a₂: τ₂} ⊓ {a₃: τ₃} ⊓ {a₄: τ₄} ⊔ ¬{a₂: ⊥} <: {a₁: τ₁}
// {a₁: τ₁} ⊓ {a₂: τ₂} ⊓ {a₃: τ₃} ⊓ {a₄: τ₄} ⊔ ¬{a₂: ⊥} <: {a₃: τ₃}
// {a₁: τ₁} ⊓ {a₂: τ₂} ⊓ {a₃: τ₃} ⊓ {a₄: τ₄} ⊔ ¬{a₂: ⊥} <: {a₄: τ₄}
{a1: #A1} & {a2: #A2} & {a3: #A3} & {a4: #A4} | ~{a2: bot} <: {a1: #A1}
{a1: #A1} & {a2: #A2} & {a3: #A3} & {a4: #A4} | ~{a2: bot} <: {a3: #A3}
{a1: #A1} & {a2: #A2} & {a3: #A3} & {a4: #A4} | ~{a2: bot} <: {a4: #A4}

// α ↦ {a: Int}
// β ↦ Int
//   |-
// {a: Int} <: α
// α <: {a: β}
'a == {a: #Int}
'b == #Int
  |-
{a: #Int} <: 'a
'a <: {a: 'b}

Feature	Type syntax
Basic Types `S, T`
top	`top`
bottom	`bot`
intersection	`S & T`
union	`S \| T`
negation	`~T`
nominal tag¹	`#A`
record	`{ a: S, b: T }`
function	`S -> T`
variable	`'a`
Input format
type alias	`'a == T`
subtyping relation	`S <: T`
subtyping problem	`'a == {a: 'a} 'b == {a: 'b} \|- 'a <: 'b 'b <: 'a`

Sebas online demonstration

Syntax Reference