Prototyping type normalizaton (#466)

* Added type normalization
2022-04-28 15:00:55 -05:00 · 2022-04-28 15:00:55 -05:00 · 74c84815a0
parent e0a6461173
commit 74c84815a0
13 changed files with 940 additions and 138 deletions
--- a/prototyping/Luau/FunctionTypes.agda
+++ b/prototyping/Luau/FunctionTypes.agda
@ -0,0 +1,38 @@
+{-# OPTIONS --rewriting #-}
+
+open import FFI.Data.Either using (Either; Left; Right)
+open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+open import Luau.TypeNormalization using (normalize)
+
+module Luau.FunctionTypes where
+
+-- The domain of a normalized type
+srcⁿ : Type → Type
+srcⁿ (S ⇒ T) = S
+srcⁿ (S ∩ T) = srcⁿ S ∪ srcⁿ T
+srcⁿ never = unknown
+srcⁿ T = never
+
+-- To get the domain of a type, we normalize it first We need to do
+-- this, since if we try to use it on non-normalized types, we get
+--
+-- src(number ∩ string) = src(number) ∪ src(string) = never ∪ never
+-- src(never) = unknown
+--
+-- so src doesn't respect type equivalence.
+src : Type → Type
+src (S ⇒ T) = S
+src T = srcⁿ(normalize T)
+
+-- The codomain of a type
+tgt : Type → Type
+tgt nil = never
+tgt (S ⇒ T) = T
+tgt never = never
+tgt unknown = unknown
+tgt number = never
+tgt boolean = never
+tgt string = never
+tgt (S ∪ T) = (tgt S) ∪ (tgt T)
+tgt (S ∩ T) = (tgt S) ∩ (tgt T)
+
--- a/prototyping/Luau/StrictMode.agda
+++ b/prototyping/Luau/StrictMode.agda
@ -5,7 +5,8 @@ module Luau.StrictMode where
 open import Agda.Builtin.Equality using (_≡_)
 open import FFI.Data.Maybe using (just; nothing)
 open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; var; binexp; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; local_←_; _∙_; done; return; name; +; -; *; /; <; >; <=; >=; ··)
-open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; _∪_; _∩_; src; tgt)
+open import Luau.FunctionTypes using (src; tgt)
+open import Luau.Type using (Type; nil; number; string; boolean; _⇒_; _∪_; _∩_)
 open import Luau.Subtyping using (_≮:_)
 open import Luau.Heap using (Heap; function_is_end) renaming (_[_] to _[_]ᴴ)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
--- a/prototyping/Luau/Subtyping.agda
+++ b/prototyping/Luau/Subtyping.agda
@ -25,7 +25,6 @@ data Language where
  function : ∀ {T U} → Language (T ⇒ U) function
  function-ok : ∀ {T U u} → (Language U u) → Language (T ⇒ U) (function-ok u)
  function-err : ∀ {T U t} → (¬Language T t) → Language (T ⇒ U) (function-err t)
-  scalar-function-err : ∀ {S t} → (Scalar S) → Language S (function-err t)
  left : ∀ {T U t} → Language T t → Language (T ∪ U) t
  right : ∀ {T U u} → Language U u → Language (T ∪ U) u
  _,_ : ∀ {T U t} → Language T t → Language U t → Language (T ∩ U) t
@ -36,6 +35,7 @@ data ¬Language where
  scalar-scalar : ∀ {S T} → (s : Scalar S) → (Scalar T) → (S ≢ T) → ¬Language T (scalar s)
  scalar-function : ∀ {S} → (Scalar S) → ¬Language S function
  scalar-function-ok : ∀ {S u} → (Scalar S) → ¬Language S (function-ok u)
+  scalar-function-err : ∀ {S t} → (Scalar S) → ¬Language S (function-err t)
  function-scalar : ∀ {S T U} (s : Scalar S) → ¬Language (T ⇒ U) (scalar s)
  function-ok : ∀ {T U u} → (¬Language U u) → ¬Language (T ⇒ U) (function-ok u)
  function-err : ∀ {T U t} → (Language T t) → ¬Language (T ⇒ U) (function-err t)
--- a/prototyping/Luau/Type.agda
+++ b/prototyping/Luau/Type.agda
@ -24,6 +24,8 @@ data Scalar : Type → Set where
  string : Scalar string
  nil : Scalar nil

+skalar = number ∪ (string ∪ (nil ∪ boolean))
+
 lhs : Type → Type
 lhs (T ⇒ _) = T
 lhs (T ∪ _) = T
@ -146,28 +148,6 @@ just T ≡ᴹᵀ just U with T ≡ᵀ U
 (just T ≡ᴹᵀ just T) | yes refl = yes refl
 (just T ≡ᴹᵀ just U) | no p = no (λ q → p (just-inv q))

-src : Type → Type
-src nil = never
-src number = never
-src boolean = never
-src string = never
-src (S ⇒ T) = S
-src (S ∪ T) = (src S) ∩ (src T)
-src (S ∩ T) = (src S) ∪ (src T)
-src never = unknown
-src unknown = never
-
-tgt : Type → Type
-tgt nil = never
-tgt (S ⇒ T) = T
-tgt never = never
-tgt unknown = unknown
-tgt number = never
-tgt boolean = never
-tgt string = never
-tgt (S ∪ T) = (tgt S) ∪ (tgt T)
-tgt (S ∩ T) = (tgt S) ∩ (tgt T)
-
 optional : Type → Type
 optional nil = nil
 optional (T ∪ nil) = (T ∪ nil)
--- a/prototyping/Luau/TypeCheck.agda
+++ b/prototyping/Luau/TypeCheck.agda
@ -7,8 +7,9 @@ open import FFI.Data.Maybe using (Maybe; just)
 open import Luau.Syntax using (Expr; Stat; Block; BinaryOperator; yes; nil; addr; number; bool; string; val; var; var_∈_; _⟨_⟩∈_; function_is_end; _$_; block_is_end; binexp; local_←_; _∙_; done; return; name; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
 open import Luau.Var using (Var)
 open import Luau.Addr using (Addr)
+open import Luau.FunctionTypes using (src; tgt)
 open import Luau.Heap using (Heap; Object; function_is_end) renaming (_[_] to _[_]ᴴ)
-open import Luau.Type using (Type; nil; unknown; number; boolean; string; _⇒_; src; tgt)
+open import Luau.Type using (Type; nil; unknown; number; boolean; string; _⇒_)
 open import Luau.VarCtxt using (VarCtxt; ∅; _⋒_; _↦_; _⊕_↦_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import FFI.Data.Vector using (Vector)
 open import FFI.Data.Maybe using (Maybe; just; nothing)
--- a/prototyping/Luau/TypeNormalization.agda
+++ b/prototyping/Luau/TypeNormalization.agda
@ -0,0 +1,69 @@
+module Luau.TypeNormalization where
+
+open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+
+-- The top non-function type
+¬function : Type
+¬function = number ∪ (string ∪ (nil ∪ boolean))
+
+-- Unions and intersections of normalized types
+_∪ᶠ_ : Type → Type → Type
+_∪ⁿˢ_ : Type → Type → Type
+_∩ⁿˢ_ : Type → Type → Type
+_∪ⁿ_ : Type → Type → Type
+_∩ⁿ_ : Type → Type → Type
+
+-- Union of function types
+(F₁ ∩ F₂) ∪ᶠ G = (F₁ ∪ᶠ G) ∩ (F₂ ∪ᶠ G)
+F ∪ᶠ (G₁ ∩ G₂) = (F ∪ᶠ G₁) ∩ (F ∪ᶠ G₂)
+(R ⇒ S) ∪ᶠ (T ⇒ U) = (R ∩ⁿ T) ⇒ (S ∪ⁿ U)
+F ∪ᶠ G = F ∪ G
+
+-- Union of normalized types
+S ∪ⁿ (T₁ ∪ T₂) = (S ∪ⁿ T₁) ∪ T₂
+S ∪ⁿ unknown = unknown
+S ∪ⁿ never = S
+unknown ∪ⁿ T = unknown
+never ∪ⁿ T = T
+(S₁ ∪ S₂) ∪ⁿ G = (S₁ ∪ⁿ G) ∪ S₂
+F ∪ⁿ G = F ∪ᶠ G
+
+-- Intersection of normalized types
+S ∩ⁿ (T₁ ∪ T₂) = (S ∩ⁿ T₁) ∪ⁿˢ (S ∩ⁿˢ T₂)
+S ∩ⁿ unknown = S
+S ∩ⁿ never = never
+(S₁ ∪ S₂) ∩ⁿ G = (S₁ ∩ⁿ G)
+unknown ∩ⁿ G = G
+never ∩ⁿ G = never
+F ∩ⁿ G = F ∩ G
+
+-- Intersection of normalized types with a scalar
+(S₁ ∪ nil) ∩ⁿˢ nil = nil
+(S₁ ∪ boolean) ∩ⁿˢ boolean = boolean
+(S₁ ∪ number) ∩ⁿˢ number = number
+(S₁ ∪ string) ∩ⁿˢ string = string
+(S₁ ∪ S₂) ∩ⁿˢ T = S₁ ∩ⁿˢ T
+unknown ∩ⁿˢ T = T
+F ∩ⁿˢ T = never
+
+-- Union of normalized types with an optional scalar
+S ∪ⁿˢ never = S
+unknown ∪ⁿˢ T = unknown
+(S₁ ∪ nil) ∪ⁿˢ nil = S₁ ∪ nil
+(S₁ ∪ boolean) ∪ⁿˢ boolean = S₁ ∪ boolean
+(S₁ ∪ number) ∪ⁿˢ number = S₁ ∪ number
+(S₁ ∪ string) ∪ⁿˢ string = S₁ ∪ string
+(S₁ ∪ S₂) ∪ⁿˢ T = (S₁ ∪ⁿˢ T) ∪ S₂
+F ∪ⁿˢ T = F ∪ T
+
+-- Normalize!
+normalize : Type → Type
+normalize nil = never ∪ nil
+normalize (S ⇒ T) = (normalize S ⇒ normalize T)
+normalize never = never
+normalize unknown = unknown
+normalize boolean = never ∪ boolean
+normalize number = never ∪ number
+normalize string = never ∪ string
+normalize (S ∪ T) = normalize S ∪ⁿ normalize T
+normalize (S ∩ T) = normalize S ∩ⁿ normalize T
--- a/prototyping/Properties.agda
+++ b/prototyping/Properties.agda
@ -4,10 +4,13 @@ module Properties where

 import Properties.Contradiction
 import Properties.Dec
+import Properties.DecSubtyping
 import Properties.Equality
 import Properties.Functions
+import Properties.FunctionTypes
 import Properties.Remember
 import Properties.Step
 import Properties.StrictMode
 import Properties.Subtyping
 import Properties.TypeCheck
+import Properties.TypeNormalization
--- a/prototyping/Properties/DecSubtyping.agda
+++ b/prototyping/Properties/DecSubtyping.agda
@ -0,0 +1,70 @@
+{-# OPTIONS --rewriting #-}
+
+module Properties.DecSubtyping where
+
+open import Agda.Builtin.Equality using (_≡_; refl)
+open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
+open import Luau.FunctionTypes using (src; srcⁿ; tgt)
+open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+open import Properties.Contradiction using (CONTRADICTION; ¬)
+open import Properties.Functions using (_∘_)
+open import Properties.Subtyping using (<:-refl; <:-trans; ≮:-trans-<:; <:-trans-≮:; <:-never; <:-unknown; <:-∪-left; <:-∪-right; <:-∪-lub;  ≮:-∪-left; ≮:-∪-right; <:-∩-left; <:-∩-right; <:-∩-glb;  ≮:-∩-left; ≮:-∩-right; dec-language; scalar-<:; <:-everything; <:-function; ≮:-function-left; ≮:-function-right)
+open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:)
+open import Properties.FunctionTypes using (fun-¬scalar; ¬fun-scalar; fun-function; src-unknown-≮:; tgt-never-≮:; src-tgtᶠ-<:)
+open import Properties.Equality using (_≢_)
+
+-- Honest this terminates, since src and tgt reduce the depth of nested arrows
+{-# TERMINATING #-}
+dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U)
+dec-subtypingᶠ : ∀ {T U} → FunType T → FunType U → Either (T ≮: U) (T <: U)
+dec-subtypingᶠⁿ : ∀ {T U} → FunType T → Normal U → Either (T ≮: U) (T <: U)
+dec-subtypingⁿ : ∀ {T U} → Normal T → Normal U → Either (T ≮: U) (T <: U)
+dec-subtyping : ∀ T U → Either (T ≮: U) (T <: U)
+
+dec-subtypingˢⁿ T U with dec-language _ (scalar T)
+dec-subtypingˢⁿ T U | Left p = Left (witness (scalar T) (scalar T) p)
+dec-subtypingˢⁿ T U | Right p = Right (scalar-<: T p)
+
+dec-subtypingᶠ {T = T} _ (U ⇒ V) with dec-subtypingⁿ U (normal (src T)) | dec-subtypingⁿ (normal (tgt T)) V
+dec-subtypingᶠ {T = T} _ (U ⇒ V) | Left p | q = Left (≮:-trans-<: (src-unknown-≮: (≮:-trans-<: p (<:-normalize (src T)))) (<:-function <:-refl <:-unknown))
+dec-subtypingᶠ {T = T} _ (U ⇒ V) | Right p | Left q = Left (≮:-trans-<: (tgt-never-≮: (<:-trans-≮: (normalize-<: (tgt T)) q)) (<:-trans (<:-function <:-never <:-refl) <:-∪-right))
+dec-subtypingᶠ T (U ⇒ V) | Right p | Right q = Right (src-tgtᶠ-<: T (<:-trans p (normalize-<: _)) (<:-trans (<:-normalize _) q))
+
+dec-subtypingᶠ T (U ∩ V) with dec-subtypingᶠ T U | dec-subtypingᶠ T V
+dec-subtypingᶠ T (U ∩ V) | Left p | q = Left (≮:-∩-left p)
+dec-subtypingᶠ T (U ∩ V) | Right p | Left q = Left (≮:-∩-right q)
+dec-subtypingᶠ T (U ∩ V) | Right p | Right q = Right (<:-∩-glb p q)
+
+dec-subtypingᶠⁿ T never = Left (witness function (fun-function T) never)
+dec-subtypingᶠⁿ T unknown = Right <:-unknown
+dec-subtypingᶠⁿ T (U ⇒ V) = dec-subtypingᶠ T (U ⇒ V)
+dec-subtypingᶠⁿ T (U ∩ V) = dec-subtypingᶠ T (U ∩ V)
+dec-subtypingᶠⁿ T (U ∪ V) with dec-subtypingᶠⁿ T U
+dec-subtypingᶠⁿ T (U ∪ V) | Left (witness t p q) = Left (witness t p (q , ¬fun-scalar V T p))
+dec-subtypingᶠⁿ T (U ∪ V) | Right p = Right (<:-trans p <:-∪-left)
+
+dec-subtypingⁿ never U = Right <:-never
+dec-subtypingⁿ unknown unknown = Right <:-refl
+dec-subtypingⁿ unknown U with dec-subtypingᶠⁿ (never ⇒ unknown) U
+dec-subtypingⁿ unknown U | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ with dec-subtypingˢⁿ number U
+dec-subtypingⁿ unknown U | Right p₁ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ with dec-subtypingˢⁿ string U
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ with dec-subtypingˢⁿ nil U
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ with dec-subtypingˢⁿ boolean U
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Left p = Left (<:-trans-≮: <:-unknown p)
+dec-subtypingⁿ unknown U | Right p₁ | Right p₂ | Right p₃ | Right p₄ | Right p₅ = Right (<:-trans <:-everything (<:-∪-lub p₁ (<:-∪-lub p₂ (<:-∪-lub p₃ (<:-∪-lub p₄ p₅)))))
+dec-subtypingⁿ (S ⇒ T) U = dec-subtypingᶠⁿ (S ⇒ T) U
+dec-subtypingⁿ (S ∩ T) U = dec-subtypingᶠⁿ (S ∩ T) U
+dec-subtypingⁿ (S ∪ T) U with dec-subtypingⁿ S U | dec-subtypingˢⁿ T U
+dec-subtypingⁿ (S ∪ T) U | Left p | q = Left (≮:-∪-left p)
+dec-subtypingⁿ (S ∪ T) U | Right p | Left q = Left (≮:-∪-right q)
+dec-subtypingⁿ (S ∪ T) U | Right p | Right q = Right (<:-∪-lub p q)
+
+dec-subtyping T U with dec-subtypingⁿ (normal T) (normal U)
+dec-subtyping T U | Left p = Left (<:-trans-≮: (normalize-<: T) (≮:-trans-<: p (<:-normalize U)))
+dec-subtyping T U | Right p = Right (<:-trans (<:-normalize T) (<:-trans p (normalize-<: U)))
+
--- a/prototyping/Properties/FunctionTypes.agda
+++ b/prototyping/Properties/FunctionTypes.agda
@ -0,0 +1,150 @@
+{-# OPTIONS --rewriting #-}
+
+module Properties.FunctionTypes where
+
+open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
+open import Luau.FunctionTypes using (srcⁿ; src; tgt)
+open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
+open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
+open import Properties.Functions using (_∘_)
+open import Properties.Subtyping using (<:-refl; ≮:-refl; <:-trans-≮:; skalar-scalar; <:-impl-⊇; skalar-function-ok; language-comp)
+open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:)
+
+-- Properties of src
+function-err-srcⁿ : ∀ {T t} → (FunType T) → (¬Language (srcⁿ T) t) → Language T (function-err t)
+function-err-srcⁿ (S ⇒ T) p = function-err p
+function-err-srcⁿ (S ∩ T) (p₁ , p₂) = (function-err-srcⁿ S p₁ , function-err-srcⁿ T p₂)
+
+¬function-err-srcᶠ : ∀ {T t} → (FunType T) → (Language (srcⁿ T) t) → ¬Language T (function-err t)
+¬function-err-srcᶠ (S ⇒ T) p = function-err p
+¬function-err-srcᶠ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p)
+¬function-err-srcᶠ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p)
+
+¬function-err-srcⁿ : ∀ {T t} → (Normal T) → (Language (srcⁿ T) t) → ¬Language T (function-err t)
+¬function-err-srcⁿ never p = never
+¬function-err-srcⁿ unknown (scalar ())
+¬function-err-srcⁿ (S ⇒ T) p = function-err p
+¬function-err-srcⁿ (S ∩ T) (left p) = left (¬function-err-srcᶠ S p)
+¬function-err-srcⁿ (S ∩ T) (right p) = right (¬function-err-srcᶠ T p)
+¬function-err-srcⁿ (S ∪ T) (scalar ())
+
+¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t)
+¬function-err-src {T = S ⇒ T} p = function-err p
+¬function-err-src {T = nil} p = scalar-function-err nil
+¬function-err-src {T = never} p = never
+¬function-err-src {T = unknown} (scalar ())
+¬function-err-src {T = boolean} p = scalar-function-err boolean
+¬function-err-src {T = number} p = scalar-function-err number
+¬function-err-src {T = string} p = scalar-function-err string
+¬function-err-src {T = S ∪ T} p = <:-impl-⊇ (<:-normalize (S ∪ T)) _ (¬function-err-srcⁿ (normal (S ∪ T)) p)
+¬function-err-src {T = S ∩ T} p = <:-impl-⊇ (<:-normalize (S ∩ T)) _ (¬function-err-srcⁿ (normal (S ∩ T)) p)
+
+src-¬function-errᶠ : ∀ {T t} → (FunType T) → Language T (function-err t) → (¬Language (srcⁿ T) t)
+src-¬function-errᶠ (S ⇒ T) (function-err p) = p
+src-¬function-errᶠ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)
+
+src-¬function-errⁿ : ∀ {T t} → (Normal T) → Language T (function-err t) → (¬Language (srcⁿ T) t)
+src-¬function-errⁿ unknown p = never
+src-¬function-errⁿ (S ⇒ T) (function-err p) = p
+src-¬function-errⁿ (S ∩ T) (p₁ , p₂) = (src-¬function-errᶠ S p₁ , src-¬function-errᶠ T p₂)
+src-¬function-errⁿ (S ∪ T) p = never
+
+src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t)
+src-¬function-err {T = S ⇒ T} (function-err p) = p
+src-¬function-err {T = unknown} p = never
+src-¬function-err {T = S ∪ T} p = src-¬function-errⁿ (normal (S ∪ T)) (<:-normalize (S ∪ T) _ p)
+src-¬function-err {T = S ∩ T} p = src-¬function-errⁿ (normal (S ∩ T)) (<:-normalize (S ∩ T) _ p)
+
+fun-¬scalar : ∀ {S T} (s : Scalar S) → FunType T → ¬Language T (scalar s)
+fun-¬scalar s (S ⇒ T) = function-scalar s
+fun-¬scalar s (S ∩ T) = left (fun-¬scalar s S)
+
+¬fun-scalar : ∀ {S T t} (s : Scalar S) → FunType T → Language T t → ¬Language S t
+¬fun-scalar s (S ⇒ T) function = scalar-function s
+¬fun-scalar s (S ⇒ T) (function-ok p) = scalar-function-ok s
+¬fun-scalar s (S ⇒ T) (function-err p) = scalar-function-err s
+¬fun-scalar s (S ∩ T) (p₁ , p₂) = ¬fun-scalar s T p₂
+
+fun-function : ∀ {T} → FunType T → Language T function
+fun-function (S ⇒ T) = function
+fun-function (S ∩ T) = (fun-function S , fun-function T)
+
+srcⁿ-¬scalar : ∀ {S T t} (s : Scalar S) → Normal T → Language T (scalar s) → (¬Language (srcⁿ T) t)
+srcⁿ-¬scalar s never (scalar ())
+srcⁿ-¬scalar s unknown p = never
+srcⁿ-¬scalar s (S ⇒ T) (scalar ())
+srcⁿ-¬scalar s (S ∩ T) (p₁ , p₂) = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s S) p₁)
+srcⁿ-¬scalar s (S ∪ T) p = never
+
+src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t)
+src-¬scalar {T = nil} s p = never
+src-¬scalar {T = T ⇒ U} s (scalar ())
+src-¬scalar {T = never} s (scalar ())
+src-¬scalar {T = unknown} s p = never
+src-¬scalar {T = boolean} s p = never
+src-¬scalar {T = number} s p = never
+src-¬scalar {T = string} s p = never
+src-¬scalar {T = T ∪ U} s p = srcⁿ-¬scalar s (normal (T ∪ U)) (<:-normalize (T ∪ U) (scalar s) p)
+src-¬scalar {T = T ∩ U} s p = srcⁿ-¬scalar s (normal (T ∩ U)) (<:-normalize (T ∩ U) (scalar s) p)
+
+srcⁿ-unknown-≮: : ∀ {T U} → (Normal U) → (T ≮: srcⁿ U) → (U ≮: (T ⇒ unknown))
+srcⁿ-unknown-≮: never (witness t p q) = CONTRADICTION (language-comp t q unknown)
+srcⁿ-unknown-≮: unknown (witness t p q) = witness (function-err t) unknown (function-err p)
+srcⁿ-unknown-≮: (U ⇒ V) (witness t p q) = witness (function-err t) (function-err q) (function-err p)
+srcⁿ-unknown-≮: (U ∩ V) (witness t p q) = witness (function-err t) (function-err-srcⁿ (U ∩ V) q) (function-err p)
+srcⁿ-unknown-≮: (U ∪ V) (witness t p q) = witness (scalar V) (right (scalar V)) (function-scalar V)
+
+src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown))
+src-unknown-≮: {U = nil} (witness t p q) = witness (scalar nil) (scalar nil) (function-scalar nil)
+src-unknown-≮: {U = T ⇒ U} (witness t p q) = witness (function-err t) (function-err q) (function-err p)
+src-unknown-≮: {U = never} (witness t p q) = CONTRADICTION (language-comp t q unknown)
+src-unknown-≮: {U = unknown} (witness t p q) = witness (function-err t) unknown (function-err p)
+src-unknown-≮: {U = boolean} (witness t p q) = witness (scalar boolean) (scalar boolean) (function-scalar boolean)
+src-unknown-≮: {U = number} (witness t p q) = witness (scalar number) (scalar number) (function-scalar number)
+src-unknown-≮: {U = string} (witness t p q) = witness (scalar string) (scalar string) (function-scalar string)
+src-unknown-≮: {U = T ∪ U} p = <:-trans-≮: (normalize-<: (T ∪ U)) (srcⁿ-unknown-≮: (normal (T ∪ U)) p)
+src-unknown-≮: {U = T ∩ U} p = <:-trans-≮: (normalize-<: (T ∩ U)) (srcⁿ-unknown-≮: (normal (T ∩ U)) p)
+
+unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T)
+unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p)
+unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q)))
+unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ())))
+unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
+
+-- Properties of tgt
+tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t)
+tgt-function-ok {T = nil} (scalar ())
+tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p
+tgt-function-ok {T = never} (scalar ())
+tgt-function-ok {T = unknown} p = unknown
+tgt-function-ok {T = boolean} (scalar ())
+tgt-function-ok {T = number} (scalar ())
+tgt-function-ok {T = string} (scalar ())
+tgt-function-ok {T = T₁ ∪ T₂} (left p) = left (tgt-function-ok p)
+tgt-function-ok {T = T₁ ∪ T₂} (right p) = right (tgt-function-ok p)
+tgt-function-ok {T = T₁ ∩ T₂} (p₁ , p₂) = (tgt-function-ok p₁ , tgt-function-ok p₂)
+
+function-ok-tgt : ∀ {T t} → Language T (function-ok t) → (Language (tgt T) t)
+function-ok-tgt (function-ok p) = p
+function-ok-tgt (left p) = left (function-ok-tgt p)
+function-ok-tgt (right p) = right (function-ok-tgt p)
+function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂)
+function-ok-tgt unknown = unknown
+
+tgt-never-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (never ⇒ U)))
+tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q)
+
+never-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (never ⇒ U))) → (tgt T ≮: U)
+never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁))
+never-tgt-≮: (witness function p (q₁ , scalar-function ()))
+never-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂
+never-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ())))
+
+src-tgtᶠ-<: : ∀ {T U V} → (FunType T) → (U <: src T) → (tgt T <: V) → (T <: (U ⇒ V))
+src-tgtᶠ-<: T p q (scalar s) r = CONTRADICTION (language-comp (scalar s) (fun-¬scalar s T) r)
+src-tgtᶠ-<: T p q function r = function
+src-tgtᶠ-<: T p q (function-ok s) r = function-ok (q s (function-ok-tgt r))
+src-tgtᶠ-<: T p q (function-err s) r = function-err (<:-impl-⊇ p s (src-¬function-err r))
+
+
--- a/prototyping/Properties/StrictMode.agda
+++ b/prototyping/Properties/StrictMode.agda
@ -11,7 +11,8 @@ open import Luau.StrictMode using (Warningᴱ; Warningᴮ; Warningᴼ; Warning
 open import Luau.Substitution using (_[_/_]ᴮ; _[_/_]ᴱ; _[_/_]ᴮunless_; var_[_/_]ᴱwhenever_)
 open import Luau.Subtyping using (_≮:_; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_; Tree; Language; ¬Language)
 open import Luau.Syntax using (Expr; yes; var; val; var_∈_; _⟨_⟩∈_; _$_; addr; number; bool; string; binexp; nil; function_is_end; block_is_end; done; return; local_←_; _∙_; fun; arg; name; ==; ~=)
-open import Luau.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; src; tgt; _≡ᵀ_; _≡ᴹᵀ_)
+open import Luau.FunctionTypes using (src; tgt)
+open import Luau.Type using (Type; nil; number; boolean; string; _⇒_; never; unknown; _∩_; _∪_; _≡ᵀ_; _≡ᴹᵀ_)
 open import Luau.TypeCheck using (_⊢ᴮ_∈_; _⊢ᴱ_∈_; _⊢ᴴᴮ_▷_∈_; _⊢ᴴᴱ_▷_∈_; nil; var; addr; app; function; block; done; return; local; orUnknown; srcBinOp; tgtBinOp)
 open import Luau.Var using (_≡ⱽ_)
 open import Luau.Addr using (_≡ᴬ_)
@ -22,7 +23,8 @@ open import Properties.Equality using (_≢_; sym; cong; trans; subst₁)
 open import Properties.Dec using (Dec; yes; no)
 open import Properties.Contradiction using (CONTRADICTION; ¬)
 open import Properties.Functions using (_∘_)
-open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never)
+open import Properties.FunctionTypes using (never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:)
+open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never)
 open import Properties.TypeCheck using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴ)
 open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··)
 open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)
--- a/prototyping/Properties/Subtyping.agda
+++ b/prototyping/Properties/Subtyping.agda
@ -4,9 +4,10 @@ module Properties.Subtyping where

 open import Agda.Builtin.Equality using (_≡_; refl)
 open import FFI.Data.Either using (Either; Left; Right; mapLR; swapLR; cond)
+open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import Luau.Subtyping using (_<:_; _≮:_; Tree; Language; ¬Language; witness; unknown; never; scalar; function; scalar-function; scalar-function-ok; scalar-function-err; scalar-scalar; function-scalar; function-ok; function-err; left; right; _,_)
-open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src; tgt)
-open import Properties.Contradiction using (CONTRADICTION; ¬)
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; skalar)
+open import Properties.Contradiction using (CONTRADICTION; ¬; ⊥)
 open import Properties.Equality using (_≢_)
 open import Properties.Functions using (_∘_)
 open import Properties.Product using (_×_; _,_)
@ -19,28 +20,28 @@ dec-language nil (scalar string) = Left (scalar-scalar string nil (λ ()))
 dec-language nil (scalar nil) = Right (scalar nil)
 dec-language nil function = Left (scalar-function nil)
 dec-language nil (function-ok t) = Left (scalar-function-ok nil)
-dec-language nil (function-err t) = Right (scalar-function-err nil)
+dec-language nil (function-err t) = Left (scalar-function-err nil)
 dec-language boolean (scalar number) = Left (scalar-scalar number boolean (λ ()))
 dec-language boolean (scalar boolean) = Right (scalar boolean)
 dec-language boolean (scalar string) = Left (scalar-scalar string boolean (λ ()))
 dec-language boolean (scalar nil) = Left (scalar-scalar nil boolean (λ ()))
 dec-language boolean function = Left (scalar-function boolean)
 dec-language boolean (function-ok t) = Left (scalar-function-ok boolean)
-dec-language boolean (function-err t) = Right (scalar-function-err boolean)
+dec-language boolean (function-err t) = Left (scalar-function-err boolean)
 dec-language number (scalar number) = Right (scalar number)
 dec-language number (scalar boolean) = Left (scalar-scalar boolean number (λ ()))
 dec-language number (scalar string) = Left (scalar-scalar string number (λ ()))
 dec-language number (scalar nil) = Left (scalar-scalar nil number (λ ()))
 dec-language number function = Left (scalar-function number)
 dec-language number (function-ok t) = Left (scalar-function-ok number)
-dec-language number (function-err t) = Right (scalar-function-err number)
+dec-language number (function-err t) = Left (scalar-function-err number)
 dec-language string (scalar number) = Left (scalar-scalar number string (λ ()))
 dec-language string (scalar boolean) = Left (scalar-scalar boolean string (λ ()))
 dec-language string (scalar string) = Right (scalar string)
 dec-language string (scalar nil) = Left (scalar-scalar nil string (λ ()))
 dec-language string function = Left (scalar-function string)
 dec-language string (function-ok t) = Left (scalar-function-ok string)
-dec-language string (function-err t) = Right (scalar-function-err string)
+dec-language string (function-err t) = Left (scalar-function-err string)
 dec-language (T₁ ⇒ T₂) (scalar s) = Left (function-scalar s)
 dec-language (T₁ ⇒ T₂) function = Right function
 dec-language (T₁ ⇒ T₂) (function-ok t) = mapLR function-ok function-ok (dec-language T₂ t)
@ -73,6 +74,11 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-impl-¬≮: : ∀ {T U} → (T <: U) → ¬(T ≮: U)
 <:-impl-¬≮: p (witness t q r) = language-comp t r (p t q)

+<:-impl-⊇ : ∀ {T U} → (T <: U) → ∀ t → ¬Language U t → ¬Language T t
+<:-impl-⊇ {T} p t q with dec-language T t
+<:-impl-⊇ {_} p t q | Left r = r
+<:-impl-⊇ {_} p t q | Right r = CONTRADICTION (language-comp t q (p t r))
+
 -- reflexivity
 ≮:-refl : ∀ {T} → ¬(T ≮: T)
 ≮:-refl (witness t p q) = language-comp t q p
@ -91,10 +97,162 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 ≮:-trans {T = T} (witness t p q) = mapLR (witness t p) (λ z → witness t z q) (dec-language T t)

 <:-trans : ∀ {S T U} → (S <: T) → (T <: U) → (S <: U)
-<:-trans p q = ¬≮:-impl-<: (cond (<:-impl-¬≮: p) (<:-impl-¬≮: q) ∘ ≮:-trans)
+<:-trans p q t r = q t (p t r)
+
+<:-trans-≮: : ∀ {S T U} → (S <: T) → (S ≮: U) → (T ≮: U)
+<:-trans-≮: p (witness t q r) = witness t (p t q) r
+
+≮:-trans-<: : ∀ {S T U} → (S ≮: U) → (T <: U) → (S ≮: T)
+≮:-trans-<: (witness t p q) r = witness t p (<:-impl-⊇ r t q)
+
+-- Properties of union
+
+<:-union : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∪ S) <: (T ∪ U))
+<:-union p q t (left r) = left (p t r)
+<:-union p q t (right r) = right (q t r)
+
+<:-∪-left : ∀ {S T} → S <: (S ∪ T)
+<:-∪-left t p = left p
+
+<:-∪-right : ∀ {S T} → T <: (S ∪ T)
+<:-∪-right t p = right p
+
+<:-∪-lub : ∀ {S T U} → (S <: U) → (T <: U) → ((S ∪ T) <: U)
+<:-∪-lub p q t (left r) = p t r
+<:-∪-lub p q t (right r) = q t r
+
+<:-∪-symm : ∀ {T U} → (T ∪ U) <: (U ∪ T)
+<:-∪-symm t (left p) = right p
+<:-∪-symm t (right p) = left p
+
+<:-∪-assocl : ∀ {S T U} → (S ∪ (T ∪ U)) <: ((S ∪ T) ∪ U)
+<:-∪-assocl t (left p) = left (left p)
+<:-∪-assocl t (right (left p)) = left (right p)
+<:-∪-assocl t (right (right p)) = right p
+
+<:-∪-assocr : ∀ {S T U} → ((S ∪ T) ∪ U) <: (S ∪ (T ∪ U))
+<:-∪-assocr t (left (left p)) = left p
+<:-∪-assocr t (left (right p)) = right (left p)
+<:-∪-assocr t (right p) = right (right p)
+
+≮:-∪-left : ∀ {S T U} → (S ≮: U) → ((S ∪ T) ≮: U)
+≮:-∪-left (witness t p q) = witness t (left p) q
+
+≮:-∪-right : ∀ {S T U} → (T ≮: U) → ((S ∪ T) ≮: U)
+≮:-∪-right (witness t p q) = witness t (right p) q
+
+-- Properties of intersection
+
+<:-intersect : ∀ {R S T U} → (R <: T) → (S <: U) → ((R ∩ S) <: (T ∩ U))
+<:-intersect p q t (r₁ , r₂) = (p t r₁ , q t r₂)
+
+<:-∩-left : ∀ {S T} → (S ∩ T) <: S
+<:-∩-left t (p , _) = p
+
+<:-∩-right : ∀ {S T} → (S ∩ T) <: T
+<:-∩-right t (_ , p) = p
+
+<:-∩-glb : ∀ {S T U} → (S <: T) → (S <: U) → (S <: (T ∩ U))
+<:-∩-glb p q t r = (p t r , q t r)
+
+<:-∩-symm : ∀ {T U} → (T ∩ U) <: (U ∩ T)
+<:-∩-symm t (p₁ , p₂) = (p₂ , p₁)
+
+≮:-∩-left : ∀ {S T U} → (S ≮: T) → (S ≮: (T ∩ U))
+≮:-∩-left (witness t p q) = witness t p (left q)
+
+≮:-∩-right : ∀ {S T U} → (S ≮: U) → (S ≮: (T ∩ U))
+≮:-∩-right (witness t p q) = witness t p (right q)
+
+-- Distribution properties
+<:-∩-distl-∪ : ∀ {S T U} → (S ∩ (T ∪ U)) <: ((S ∩ T) ∪ (S ∩ U))
+<:-∩-distl-∪ t (p₁ , left p₂) = left (p₁ , p₂)
+<:-∩-distl-∪ t (p₁ , right p₂) = right (p₁ , p₂)
+
+∩-distl-∪-<: : ∀ {S T U} → ((S ∩ T) ∪ (S ∩ U)) <: (S ∩ (T ∪ U))
+∩-distl-∪-<: t (left (p₁ , p₂)) = (p₁ , left p₂)
+∩-distl-∪-<: t (right (p₁ , p₂)) = (p₁ , right p₂)
+
+<:-∩-distr-∪ : ∀ {S T U} → ((S ∪ T) ∩ U) <:  ((S ∩ U) ∪ (T ∩ U))
+<:-∩-distr-∪ t (left p₁ , p₂) = left (p₁ , p₂)
+<:-∩-distr-∪ t (right p₁ , p₂) = right (p₁ , p₂)
+
+∩-distr-∪-<: : ∀ {S T U} → ((S ∩ U) ∪ (T ∩ U)) <: ((S ∪ T) ∩ U)
+∩-distr-∪-<: t (left (p₁ , p₂)) = (left p₁ , p₂)
+∩-distr-∪-<: t (right (p₁ , p₂)) = (right p₁ , p₂)
+
+<:-∪-distl-∩ : ∀ {S T U} → (S ∪ (T ∩ U)) <: ((S ∪ T) ∩ (S ∪ U))
+<:-∪-distl-∩ t (left p) = (left p , left p)
+<:-∪-distl-∩ t (right (p₁ , p₂)) = (right p₁ , right p₂)
+
+∪-distl-∩-<: : ∀ {S T U} → ((S ∪ T) ∩ (S ∪ U)) <: (S ∪ (T ∩ U))
+∪-distl-∩-<: t (left p₁ , p₂) = left p₁
+∪-distl-∩-<: t (right p₁ , left p₂) = left p₂
+∪-distl-∩-<: t (right p₁ , right p₂) = right (p₁ , p₂)
+
+<:-∪-distr-∩ : ∀ {S T U} → ((S ∩ T) ∪ U) <: ((S ∪ U) ∩ (T ∪ U))
+<:-∪-distr-∩ t (left (p₁ , p₂)) = left p₁ , left p₂
+<:-∪-distr-∩ t (right p) = (right p , right p)
+
+∪-distr-∩-<: : ∀ {S T U} → ((S ∪ U) ∩ (T ∪ U)) <: ((S ∩ T) ∪ U)
+∪-distr-∩-<: t (left p₁ , left p₂) = left (p₁ , p₂)
+∪-distr-∩-<: t (left p₁ , right p₂) = right p₂
+∪-distr-∩-<: t (right p₁ , p₂) = right p₁
+
+-- Properties of functions
+<:-function : ∀ {R S T U} → (R <: S) → (T <: U) → (S ⇒ T) <: (R ⇒ U)
+<:-function p q function function = function
+<:-function p q (function-ok t) (function-ok r) = function-ok (q t r)
+<:-function p q (function-err s) (function-err r) = function-err (<:-impl-⊇ p s r)
+
+<:-function-∩-∪ : ∀ {R S T U} → ((R ⇒ T) ∩ (S ⇒ U)) <: ((R ∪ S) ⇒ (T ∪ U))
+<:-function-∩-∪ function (function , function) = function
+<:-function-∩-∪ (function-ok t) (function-ok p₁ , function-ok p₂) = function-ok (right p₂)
+<:-function-∩-∪ (function-err _) (function-err p₁ , function-err q₂) = function-err (p₁ , q₂)
+
+<:-function-∩ : ∀ {S T U} → ((S ⇒ T) ∩ (S ⇒ U)) <: (S ⇒ (T ∩ U))
+<:-function-∩ function (function , function) = function
+<:-function-∩ (function-ok t) (function-ok p₁ , function-ok p₂) = function-ok (p₁ , p₂)
+<:-function-∩ (function-err s) (function-err p₁ , function-err p₂) = function-err p₂
+
+<:-function-∪ : ∀ {R S T U} → ((R ⇒ S) ∪ (T ⇒ U)) <: ((R ∩ T) ⇒ (S ∪ U))
+<:-function-∪ function (left function) = function
+<:-function-∪ (function-ok t) (left (function-ok p)) = function-ok (left p)
+<:-function-∪ (function-err s) (left (function-err p)) = function-err (left p)
+<:-function-∪ (scalar s) (left (scalar ()))
+<:-function-∪ function (right function) = function
+<:-function-∪ (function-ok t) (right (function-ok p)) = function-ok (right p)
+<:-function-∪ (function-err s) (right (function-err x)) = function-err (right x)
+<:-function-∪ (scalar s) (right (scalar ()))
+
+<:-function-∪-∩ : ∀ {R S T U} → ((R ∩ S) ⇒ (T ∪ U)) <: ((R ⇒ T) ∪ (S ⇒ U))
+<:-function-∪-∩ function function = left function
+<:-function-∪-∩ (function-ok t) (function-ok (left p)) = left (function-ok p)
+<:-function-∪-∩ (function-ok t) (function-ok (right p)) = right (function-ok p)
+<:-function-∪-∩ (function-err s) (function-err (left p)) = left (function-err p)
+<:-function-∪-∩ (function-err s) (function-err (right p)) = right (function-err p)
+
+≮:-function-left : ∀ {R S T U} → (R ≮: S) → (S ⇒ T) ≮: (R ⇒ U)
+≮:-function-left (witness t p q) = witness (function-err t) (function-err q) (function-err p)
+
+≮:-function-right : ∀ {R S T U} → (T ≮: U) → (S ⇒ T) ≮: (R ⇒ U)
+≮:-function-right (witness t p q) = witness (function-ok t) (function-ok p) (function-ok q)

 -- Properties of scalars
-skalar = number ∪ (string ∪ (nil ∪ boolean))
+skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t))
+skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean)))
+
+scalar-<: : ∀ {S T} → (s : Scalar S) → Language T (scalar s) → (S <: T)
+scalar-<: number p (scalar number) (scalar number) = p
+scalar-<: boolean p (scalar boolean) (scalar boolean) = p
+scalar-<: string p (scalar string) (scalar string) = p
+scalar-<: nil p (scalar nil) (scalar nil) = p
+
+scalar-∩-function-<:-never : ∀ {S T U} → (Scalar S) → ((T ⇒ U) ∩ S) <: never
+scalar-∩-function-<:-never number .(scalar number) (() , scalar number)
+scalar-∩-function-<:-never boolean .(scalar boolean) (() , scalar boolean)
+scalar-∩-function-<:-never string .(scalar string) (() , scalar string)
+scalar-∩-function-<:-never nil .(scalar nil) (() , scalar nil)

 function-≮:-scalar : ∀ {S T U} → (Scalar U) → ((S ⇒ T) ≮: U)
 function-≮:-scalar s = witness function function (scalar-function s)
@ -111,28 +269,8 @@ scalar-≮:-never s = witness (scalar s) (scalar s) never
 scalar-≢-impl-≮: : ∀ {T U} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ≮: U)
 scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-scalar s₁ s₂ p)

-- Properties of tgt
-tgt-function-ok : ∀ {T t} → (Language (tgt T) t) → Language T (function-ok t)
-tgt-function-ok {T = nil} (scalar ())
-tgt-function-ok {T = T₁ ⇒ T₂} p = function-ok p
-tgt-function-ok {T = never} (scalar ())
-tgt-function-ok {T = unknown} p = unknown
-tgt-function-ok {T = boolean} (scalar ())
-tgt-function-ok {T = number} (scalar ())
-tgt-function-ok {T = string} (scalar ())
-tgt-function-ok {T = T₁ ∪ T₂} (left p) = left (tgt-function-ok p)
-tgt-function-ok {T = T₁ ∪ T₂} (right p) = right (tgt-function-ok p)
-tgt-function-ok {T = T₁ ∩ T₂} (p₁ , p₂) = (tgt-function-ok p₁ , tgt-function-ok p₂)
-
-function-ok-tgt : ∀ {T t} → Language T (function-ok t) → (Language (tgt T) t)
-function-ok-tgt (function-ok p) = p
-function-ok-tgt (left p) = left (function-ok-tgt p)
-function-ok-tgt (right p) = right (function-ok-tgt p)
-function-ok-tgt (p₁ , p₂) = (function-ok-tgt p₁ , function-ok-tgt p₂)
-function-ok-tgt unknown = unknown
-
-skalar-function-ok : ∀ {t} → (¬Language skalar (function-ok t))
-skalar-function-ok = (scalar-function-ok number , (scalar-function-ok string , (scalar-function-ok nil , scalar-function-ok boolean)))
+scalar-≢-∩-<:-never : ∀ {T U V} → (Scalar T) → (Scalar U) → (T ≢ U) → (T ∩ U) <: V
+scalar-≢-∩-<:-never s t p u (scalar s₁ , scalar s₂) = CONTRADICTION (p refl)

 skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s))
 skalar-scalar number = left (scalar number)
@ -140,72 +278,6 @@ skalar-scalar boolean = right (right (right (scalar boolean)))
 skalar-scalar string = right (left (scalar string))
 skalar-scalar nil = right (right (left (scalar nil)))

-tgt-never-≮: : ∀ {T U} → (tgt T ≮: U) → (T ≮: (skalar ∪ (never ⇒ U)))
-tgt-never-≮: (witness t p q) = witness (function-ok t) (tgt-function-ok p) (skalar-function-ok , function-ok q)
-
-never-tgt-≮: : ∀ {T U} → (T ≮: (skalar ∪ (never ⇒ U))) → (tgt T ≮: U)
-never-tgt-≮: (witness (scalar s) p (q₁ , q₂)) = CONTRADICTION (≮:-refl (witness (scalar s) (skalar-scalar s) q₁))
-never-tgt-≮: (witness function p (q₁ , scalar-function ()))
-never-tgt-≮: (witness (function-ok t) p (q₁ , function-ok q₂)) = witness t (function-ok-tgt p) q₂
-never-tgt-≮: (witness (function-err (scalar s)) p (q₁ , function-err (scalar ())))
-
-- Properties of src
-function-err-src : ∀ {T t} → (¬Language (src T) t) → Language T (function-err t)
-function-err-src {T = nil} never = scalar-function-err nil
-function-err-src {T = T₁ ⇒ T₂} p = function-err p
-function-err-src {T = never} (scalar-scalar number () p)
-function-err-src {T = never} (scalar-function-ok ())
-function-err-src {T = unknown} never = unknown
-function-err-src {T = boolean} p = scalar-function-err boolean
-function-err-src {T = number} p = scalar-function-err number
-function-err-src {T = string} p = scalar-function-err string
-function-err-src {T = T₁ ∪ T₂} (left p) = left (function-err-src p)
-function-err-src {T = T₁ ∪ T₂} (right p) = right (function-err-src p)
-function-err-src {T = T₁ ∩ T₂} (p₁ , p₂) = function-err-src p₁ , function-err-src p₂
-
-¬function-err-src : ∀ {T t} → (Language (src T) t) → ¬Language T (function-err t)
-¬function-err-src {T = nil} (scalar ())
-¬function-err-src {T = T₁ ⇒ T₂} p = function-err p
-¬function-err-src {T = never} unknown = never
-¬function-err-src {T = unknown} (scalar ())
-¬function-err-src {T = boolean} (scalar ())
-¬function-err-src {T = number} (scalar ())
-¬function-err-src {T = string} (scalar ())
-¬function-err-src {T = T₁ ∪ T₂} (p₁ , p₂) = (¬function-err-src p₁ , ¬function-err-src p₂)
-¬function-err-src {T = T₁ ∩ T₂} (left p) = left (¬function-err-src p)
-¬function-err-src {T = T₁ ∩ T₂} (right p) = right (¬function-err-src p)
-
-src-¬function-err : ∀ {T t} → Language T (function-err t) → (¬Language (src T) t)
-src-¬function-err {T = nil} p = never
-src-¬function-err {T = T₁ ⇒ T₂} (function-err p) = p
-src-¬function-err {T = never} (scalar-function-err ())
-src-¬function-err {T = unknown} p = never
-src-¬function-err {T = boolean} p = never
-src-¬function-err {T = number} p = never
-src-¬function-err {T = string} p = never
-src-¬function-err {T = T₁ ∪ T₂} (left p) = left (src-¬function-err p)
-src-¬function-err {T = T₁ ∪ T₂} (right p) = right (src-¬function-err p)
-src-¬function-err {T = T₁ ∩ T₂} (p₁ , p₂) = (src-¬function-err p₁ , src-¬function-err p₂)
-
-src-¬scalar : ∀ {S T t} (s : Scalar S) → Language T (scalar s) → (¬Language (src T) t)
-src-¬scalar number (scalar number) = never
-src-¬scalar boolean (scalar boolean) = never
-src-¬scalar string (scalar string) = never
-src-¬scalar nil (scalar nil) = never
-src-¬scalar s (left p) = left (src-¬scalar s p)
-src-¬scalar s (right p) = right (src-¬scalar s p)
-src-¬scalar s (p₁ , p₂) = (src-¬scalar s p₁ , src-¬scalar s p₂)
-src-¬scalar s unknown = never
-
-src-unknown-≮: : ∀ {T U} → (T ≮: src U) → (U ≮: (T ⇒ unknown))
-src-unknown-≮: (witness t p q) = witness (function-err t) (function-err-src q) (¬function-err-src p)
-
-unknown-src-≮: : ∀ {S T U} → (U ≮: S) → (T ≮: (U ⇒ unknown)) → (U ≮: src T)
-unknown-src-≮: (witness t x x₁) (witness (scalar s) p (function-scalar s)) = witness t x (src-¬scalar s p)
-unknown-src-≮: r (witness (function-ok (scalar s)) p (function-ok (scalar-scalar s () q)))
-unknown-src-≮: r (witness (function-ok (function-ok _)) p (function-ok (scalar-function-ok ())))
-unknown-src-≮: r (witness (function-err t) p (function-err q)) = witness t q (src-¬function-err p)
-
 -- Properties of unknown and never
 unknown-≮: : ∀ {T U} → (T ≮: U) → (unknown ≮: U)
 unknown-≮: (witness t p q) = witness t unknown q
@ -219,6 +291,28 @@ unknown-≮:-never = witness (scalar nil) unknown never
 function-≮:-never : ∀ {T U} → ((T ⇒ U) ≮: never)
 function-≮:-never = witness function function never

+<:-never : ∀ {T} → (never <: T)
+<:-never t (scalar ())
+
+≮:-never-left : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: T) → (S ∩ U) ≮: never
+≮:-never-left p (witness t q₁ q₂) with p t q₁
+≮:-never-left p (witness t q₁ q₂) | left r = CONTRADICTION (language-comp t q₂ r)
+≮:-never-left p (witness t q₁ q₂) | right r = witness t (q₁ , r) never
+
+≮:-never-right : ∀ {S T U} → (S <: (T ∪ U)) → (S ≮: U) → (S ∩ T) ≮: never
+≮:-never-right p (witness t q₁ q₂) with p t q₁
+≮:-never-right p (witness t q₁ q₂) | left r = witness t (q₁ , r) never
+≮:-never-right p (witness t q₁ q₂) | right r = CONTRADICTION (language-comp t q₂ r)
+
+<:-unknown : ∀ {T} → (T <: unknown)
+<:-unknown t p = unknown
+
+<:-everything : unknown <: ((never ⇒ unknown) ∪ skalar)
+<:-everything (scalar s) p = right (skalar-scalar s)
+<:-everything function p = left function
+<:-everything (function-ok t) p = left (function-ok unknown)
+<:-everything (function-err s) p = left (function-err never)
+
 -- A Gentle Introduction To Semantic Subtyping (https://www.cduce.org/papers/gentle.pdf)
 -- defines a "set-theoretic" model (sec 2.5)
 -- Unfortunately we don't quite have this property, due to uninhabited types,
@ -234,13 +328,21 @@ _⊗_ : ∀ {A B : Set} → (A → Set) → (B → Set) → ((A × B) → Set)
 Comp : ∀ {A : Set} → (A → Set) → (A → Set)
 Comp P a = ¬(P a)

+Lift : ∀ {A : Set} → (A → Set) → (Maybe A → Set)
+Lift P nothing = ⊥
+Lift P (just a) = P a
+
 set-theoretic-if : ∀ {S₁ T₁ S₂ T₂} →

  -- This is the "if" part of being a set-theoretic model
+  -- though it uses the definition from Frisch's thesis
+  -- rather than from the Gentle Introduction. The difference
+  -- being the presence of Lift, (written D_Ω in Defn 4.2 of
+  -- https://www.cduce.org/papers/frisch_phd.pdf).
  (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)) →
-  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁)) → Q ⊆ Comp((Language S₂) ⊗ Comp(Language T₂)))
+  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂))))

-set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , u) Qtu (S₂t , ¬T₂u) = q (t , u) Qtu (S₁t , ¬T₁u) where
+set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , just u) Qtu (S₂t , ¬T₂u) = q (t , just u) Qtu (S₁t , ¬T₁u) where

  S₁t : Language S₁ t
  S₁t with dec-language S₁ t
@ -252,6 +354,14 @@ set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , u) Qtu (S₂t , ¬T₂u)
  ¬T₁u T₁u with p (function-ok u) (function-ok T₁u)
  ¬T₁u T₁u | function-ok T₂u = ¬T₂u T₂u

+set-theoretic-if {S₁} {T₁} {S₂} {T₂} p Q q (t , nothing) Qt- (S₂t , _) = q (t , nothing) Qt- (S₁t , λ ()) where
+
+  S₁t : Language S₁ t
+  S₁t with dec-language S₁ t
+  S₁t | Left ¬S₁t with p (function-err t) (function-err ¬S₁t)
+  S₁t | Left ¬S₁t | function-err ¬S₂t = CONTRADICTION (language-comp t ¬S₂t S₂t)
+  S₁t | Right r = r
+
 not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →

  -- We don't quite have that this is a set-theoretic model
@ -260,32 +370,33 @@ not-quite-set-theoretic-only-if : ∀ {S₁ T₁ S₂ T₂} →
  ∀ s₂ t₂ → Language S₂ s₂ → ¬Language T₂ t₂ →

  -- This is the "only if" part of being a set-theoretic model
-  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁)) → Q ⊆ Comp((Language S₂) ⊗ Comp(Language T₂))) →
+  (∀ Q → Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁))) → Q ⊆ Comp((Language S₂) ⊗ Comp(Lift(Language T₂)))) →
  (Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂))

 not-quite-set-theoretic-only-if {S₁} {T₁} {S₂} {T₂} s₂ t₂ S₂s₂ ¬T₂t₂ p = r where

-  Q : (Tree × Tree) → Set
-  Q (t , u) = Either (¬Language S₁ t) (Language T₁ u)
+  Q : (Tree × Maybe Tree) → Set
+  Q (t , just u) = Either (¬Language S₁ t) (Language T₁ u)
+  Q (t , nothing) = ¬Language S₁ t

-  q : Q ⊆ Comp((Language S₁) ⊗ Comp(Language T₁))
-  q (t , u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t
-  q (t , u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u
+  q : Q ⊆ Comp((Language S₁) ⊗ Comp(Lift(Language T₁)))
+  q (t , just u) (Left ¬S₁t) (S₁t , ¬T₁u) = language-comp t ¬S₁t S₁t
+  q (t , just u) (Right T₂u) (S₁t , ¬T₁u) = ¬T₁u T₂u
+  q (t , nothing) ¬S₁t (S₁t , _) = language-comp t ¬S₁t S₁t

  r : Language (S₁ ⇒ T₁) ⊆ Language (S₂ ⇒ T₂)
  r function function = function
-  r (function-err t) (function-err ¬S₁t) with dec-language S₂ t
-  r (function-err t) (function-err ¬S₁t) | Left ¬S₂t = function-err ¬S₂t
-  r (function-err t) (function-err ¬S₁t) | Right S₂t = CONTRADICTION (p Q q (t , t₂) (Left ¬S₁t) (S₂t , language-comp t₂ ¬T₂t₂))
+  r (function-err s) (function-err ¬S₁s) with dec-language S₂ s
+  r (function-err s) (function-err ¬S₁s) | Left ¬S₂s = function-err ¬S₂s
+  r (function-err s) (function-err ¬S₁s) | Right S₂s = CONTRADICTION (p Q q (s , nothing) ¬S₁s (S₂s , λ ()))
  r (function-ok t) (function-ok T₁t) with dec-language T₂ t
-  r (function-ok t) (function-ok T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , t) (Right T₁t) (S₂s₂ ,  language-comp t ¬T₂t))
+  r (function-ok t) (function-ok T₁t) | Left ¬T₂t = CONTRADICTION (p Q q (s₂ , just t) (Right T₁t) (S₂s₂ , language-comp t ¬T₂t))
  r (function-ok t) (function-ok T₁t) | Right T₂t = function-ok T₂t

 -- A counterexample when the argument type is empty.

-set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Language number)) → Q ⊆ Comp((Language never) ⊗ Comp(Language string)))
+set-theoretic-counterexample-one : (∀ Q → Q ⊆ Comp((Language never) ⊗ Comp(Lift(Language number))) → Q ⊆ Comp((Language never) ⊗ Comp(Lift(Language string))))
 set-theoretic-counterexample-one Q q ((scalar s) , u) Qtu (scalar () , p)
-set-theoretic-counterexample-one Q q ((function-err t) , u) Qtu (scalar-function-err () , p)

 set-theoretic-counterexample-two : (never ⇒ number) ≮: (never ⇒ string)
 set-theoretic-counterexample-two = witness
--- a/prototyping/Properties/TypeCheck.agda
+++ b/prototyping/Properties/TypeCheck.agda
@ -8,7 +8,8 @@ open import FFI.Data.Maybe using (Maybe; just; nothing)
 open import FFI.Data.Either using (Either)
 open import Luau.TypeCheck using (_⊢ᴱ_∈_; _⊢ᴮ_∈_; ⊢ᴼ_; ⊢ᴴ_; _⊢ᴴᴱ_▷_∈_; _⊢ᴴᴮ_▷_∈_; nil; var; addr; number; bool; string; app; function; block; binexp; done; return; local; nothing; orUnknown; tgtBinOp)
 open import Luau.Syntax using (Block; Expr; Value; BinaryOperator; yes; nil; addr; number; bool; string; val; var; binexp; _$_; function_is_end; block_is_end; _∙_; return; done; local_←_; _⟨_⟩; _⟨_⟩∈_; var_∈_; name; fun; arg; +; -; *; /; <; >; ==; ~=; <=; >=)
-open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_; src; tgt)
+open import Luau.FunctionTypes using (src; tgt)
+open import Luau.Type using (Type; nil; unknown; never; number; boolean; string; _⇒_)
 open import Luau.RuntimeType using (RuntimeType; nil; number; function; string; valueType)
 open import Luau.VarCtxt using (VarCtxt; ∅; _↦_; _⊕_↦_; _⋒_; _⊝_) renaming (_[_] to _[_]ⱽ)
 open import Luau.Addr using (Addr)
--- a/prototyping/Properties/TypeNormalization.agda
+++ b/prototyping/Properties/TypeNormalization.agda
@ -0,0 +1,376 @@
+{-# OPTIONS --rewriting #-}
+
+module Properties.TypeNormalization where
+
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
+open import Luau.Subtyping using (scalar-function-err)
+open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; normalize)
+open import Luau.Subtyping using (_<:_)
+open import Properties.Subtyping using (<:-trans; <:-refl; <:-unknown; <:-never; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∩-symm; <:-function; <:-function-∪-∩; <:-function-∩-∪; <:-function-∪; <:-everything; <:-union; <:-∪-assocl; <:-∪-assocr; <:-∪-symm; <:-intersect;  ∪-distl-∩-<:; ∪-distr-∩-<:; <:-∪-distr-∩; <:-∪-distl-∩; ∩-distl-∪-<:; <:-∩-distl-∪; <:-∩-distr-∪; scalar-∩-function-<:-never; scalar-≢-∩-<:-never)
+
+-- Notmal forms for types
+data FunType : Type → Set
+data Normal : Type → Set
+
+data FunType where
+  _⇒_ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ T)
+  _∩_ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ G)
+
+data Normal where
+  never : Normal never
+  unknown : Normal unknown
+  _⇒_ : ∀ {S T} → Normal S → Normal T → Normal (S ⇒ T)
+  _∩_ : ∀ {F G} → FunType F → FunType G → Normal (F ∩ G)
+  _∪_ : ∀ {S T} → Normal S → Scalar T → Normal (S ∪ T)
+
+data OptScalar : Type → Set where
+  never : OptScalar never
+  number : OptScalar number
+  boolean : OptScalar boolean
+  string : OptScalar string
+  nil : OptScalar nil
+
+-- Normalization produces normal types
+normal : ∀ T → Normal (normalize T)
+normalᶠ : ∀ {F} → FunType F → Normal F
+normal-∪ⁿ : ∀ {S T} → Normal S → Normal T → Normal (S ∪ⁿ T)
+normal-∩ⁿ : ∀ {S T} → Normal S → Normal T → Normal (S ∩ⁿ T)
+normal-∪ⁿˢ : ∀ {S T} → Normal S → OptScalar T → Normal (S ∪ⁿˢ T)
+normal-∩ⁿˢ : ∀ {S T} → Normal S → Scalar T → OptScalar (S ∩ⁿˢ T)
+normal-∪ᶠ : ∀ {F G} → FunType F → FunType G → FunType (F ∪ᶠ G)
+
+normal nil = never ∪ nil
+normal (S ⇒ T) = normalᶠ ((normal S) ⇒ (normal T))
+normal never = never
+normal unknown = unknown
+normal boolean = never ∪ boolean
+normal number = never ∪ number
+normal string = never ∪ string
+normal (S ∪ T) = normal-∪ⁿ (normal S) (normal T)
+normal (S ∩ T) = normal-∩ⁿ (normal S) (normal T)
+
+normalᶠ (S ⇒ T) = S ⇒ T
+normalᶠ (F ∩ G) = F ∩ G
+
+normal-∪ⁿ S (T₁ ∪ T₂) = (normal-∪ⁿ S T₁) ∪ T₂
+normal-∪ⁿ S never = S
+normal-∪ⁿ S unknown = unknown
+normal-∪ⁿ never (T ⇒ U) = T ⇒ U
+normal-∪ⁿ never (G₁ ∩ G₂) = G₁ ∩ G₂
+normal-∪ⁿ unknown (T ⇒ U) = unknown
+normal-∪ⁿ unknown (G₁ ∩ G₂) = unknown
+normal-∪ⁿ (R ⇒ S) (T ⇒ U) = normalᶠ (normal-∪ᶠ (R ⇒ S) (T ⇒ U))
+normal-∪ⁿ (R ⇒ S) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (R ⇒ S) (G₁ ∩ G₂))
+normal-∪ⁿ (F₁ ∩ F₂) (T ⇒ U) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (T ⇒ U))
+normal-∪ⁿ (F₁ ∩ F₂) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (G₁ ∩ G₂))
+normal-∪ⁿ (S₁ ∪ S₂) (T₁ ⇒ T₂) = normal-∪ⁿ S₁ (T₁ ⇒ T₂) ∪ S₂
+normal-∪ⁿ (S₁ ∪ S₂) (G₁ ∩ G₂) = normal-∪ⁿ S₁ (G₁ ∩ G₂) ∪ S₂
+
+normal-∩ⁿ S never = never
+normal-∩ⁿ S unknown = S
+normal-∩ⁿ S (T ∪ U) = normal-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U )
+normal-∩ⁿ never (T ⇒ U) = never
+normal-∩ⁿ unknown (T ⇒ U) = T ⇒ U
+normal-∩ⁿ (R ⇒ S) (T ⇒ U) = (R ⇒ S) ∩ (T ⇒ U)
+normal-∩ⁿ (R ∩ S) (T ⇒ U) = (R ∩ S) ∩ (T ⇒ U)
+normal-∩ⁿ (R ∪ S) (T ⇒ U) = normal-∩ⁿ R (T ⇒ U)
+normal-∩ⁿ never (T ∩ U) = never
+normal-∩ⁿ unknown (T ∩ U) = T ∩ U
+normal-∩ⁿ (R ⇒ S) (T ∩ U) = (R ⇒ S) ∩ (T ∩ U)
+normal-∩ⁿ (R ∩ S) (T ∩ U) = (R ∩ S) ∩ (T ∩ U)
+normal-∩ⁿ (R ∪ S) (T ∩ U) = normal-∩ⁿ R (T ∩ U)
+
+normal-∪ⁿˢ S never = S
+normal-∪ⁿˢ never number = never ∪ number
+normal-∪ⁿˢ unknown number = unknown
+normal-∪ⁿˢ (R ⇒ S) number = (R ⇒ S) ∪ number
+normal-∪ⁿˢ (R ∩ S) number = (R ∩ S) ∪ number
+normal-∪ⁿˢ (R ∪ number) number = R ∪ number
+normal-∪ⁿˢ (R ∪ boolean) number = normal-∪ⁿˢ R number ∪ boolean
+normal-∪ⁿˢ (R ∪ string) number = normal-∪ⁿˢ R number ∪ string
+normal-∪ⁿˢ (R ∪ nil) number = normal-∪ⁿˢ R number ∪ nil
+normal-∪ⁿˢ never boolean = never ∪ boolean
+normal-∪ⁿˢ unknown boolean = unknown
+normal-∪ⁿˢ (R ⇒ S) boolean = (R ⇒ S) ∪ boolean
+normal-∪ⁿˢ (R ∩ S) boolean = (R ∩ S) ∪ boolean
+normal-∪ⁿˢ (R ∪ number) boolean = normal-∪ⁿˢ R boolean ∪ number
+normal-∪ⁿˢ (R ∪ boolean) boolean = R ∪ boolean
+normal-∪ⁿˢ (R ∪ string) boolean = normal-∪ⁿˢ R boolean ∪ string
+normal-∪ⁿˢ (R ∪ nil) boolean = normal-∪ⁿˢ R boolean ∪ nil
+normal-∪ⁿˢ never string = never ∪ string
+normal-∪ⁿˢ unknown string = unknown
+normal-∪ⁿˢ (R ⇒ S) string = (R ⇒ S) ∪ string
+normal-∪ⁿˢ (R ∩ S) string = (R ∩ S) ∪ string
+normal-∪ⁿˢ (R ∪ number) string = normal-∪ⁿˢ R string ∪ number
+normal-∪ⁿˢ (R ∪ boolean) string = normal-∪ⁿˢ R string ∪ boolean
+normal-∪ⁿˢ (R ∪ string) string = R ∪ string
+normal-∪ⁿˢ (R ∪ nil) string = normal-∪ⁿˢ R string ∪ nil
+normal-∪ⁿˢ never nil = never ∪ nil
+normal-∪ⁿˢ unknown nil = unknown
+normal-∪ⁿˢ (R ⇒ S) nil = (R ⇒ S) ∪ nil
+normal-∪ⁿˢ (R ∩ S) nil = (R ∩ S) ∪ nil
+normal-∪ⁿˢ (R ∪ number) nil = normal-∪ⁿˢ R nil ∪ number
+normal-∪ⁿˢ (R ∪ boolean) nil = normal-∪ⁿˢ R nil ∪ boolean
+normal-∪ⁿˢ (R ∪ string) nil = normal-∪ⁿˢ R nil ∪ string
+normal-∪ⁿˢ (R ∪ nil) nil = R ∪ nil
+
+normal-∩ⁿˢ never number = never
+normal-∩ⁿˢ never boolean = never
+normal-∩ⁿˢ never string = never
+normal-∩ⁿˢ never nil = never
+normal-∩ⁿˢ unknown number = number
+normal-∩ⁿˢ unknown boolean = boolean
+normal-∩ⁿˢ unknown string = string
+normal-∩ⁿˢ unknown nil = nil
+normal-∩ⁿˢ (R ⇒ S) number = never
+normal-∩ⁿˢ (R ⇒ S) boolean = never
+normal-∩ⁿˢ (R ⇒ S) string = never
+normal-∩ⁿˢ (R ⇒ S) nil = never
+normal-∩ⁿˢ (R ∩ S) number = never
+normal-∩ⁿˢ (R ∩ S) boolean = never
+normal-∩ⁿˢ (R ∩ S) string = never
+normal-∩ⁿˢ (R ∩ S) nil = never
+normal-∩ⁿˢ (R ∪ number) number = number
+normal-∩ⁿˢ (R ∪ boolean) number = normal-∩ⁿˢ R number
+normal-∩ⁿˢ (R ∪ string) number = normal-∩ⁿˢ R number
+normal-∩ⁿˢ (R ∪ nil) number = normal-∩ⁿˢ R number
+normal-∩ⁿˢ (R ∪ number) boolean = normal-∩ⁿˢ R boolean
+normal-∩ⁿˢ (R ∪ boolean) boolean = boolean
+normal-∩ⁿˢ (R ∪ string) boolean = normal-∩ⁿˢ R boolean
+normal-∩ⁿˢ (R ∪ nil) boolean = normal-∩ⁿˢ R boolean
+normal-∩ⁿˢ (R ∪ number) string = normal-∩ⁿˢ R string
+normal-∩ⁿˢ (R ∪ boolean) string = normal-∩ⁿˢ R string
+normal-∩ⁿˢ (R ∪ string) string = string
+normal-∩ⁿˢ (R ∪ nil) string = normal-∩ⁿˢ R string
+normal-∩ⁿˢ (R ∪ number) nil = normal-∩ⁿˢ R nil
+normal-∩ⁿˢ (R ∪ boolean) nil = normal-∩ⁿˢ R nil
+normal-∩ⁿˢ (R ∪ string) nil = normal-∩ⁿˢ R nil
+normal-∩ⁿˢ (R ∪ nil) nil = nil
+
+normal-∪ᶠ (R ⇒ S) (T ⇒ U) = (normal-∩ⁿ R T) ⇒ (normal-∪ⁿ S U)
+normal-∪ᶠ (R ⇒ S) (G ∩ H) = normal-∪ᶠ (R ⇒ S) G ∩ normal-∪ᶠ (R ⇒ S) H
+normal-∪ᶠ (E ∩ F) G = normal-∪ᶠ E G ∩ normal-∪ᶠ F G
+
+scalar-∩-fun-<:-never : ∀ {F S} → FunType F → Scalar S → (F ∩ S) <: never
+scalar-∩-fun-<:-never (T ⇒ U) S = scalar-∩-function-<:-never S
+scalar-∩-fun-<:-never (F ∩ G) S = <:-trans (<:-intersect <:-∩-left <:-refl) (scalar-∩-fun-<:-never F S)
+
+flipper : ∀ {S T U} → ((S ∪ T) ∪ U) <: ((S ∪ U) ∪ T)
+flipper = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) <:-∪-assocl)
+
+∩-<:-∩ⁿ :  ∀ {S T} → Normal S → Normal T → (S ∩ T) <: (S ∩ⁿ T)
+∩ⁿ-<:-∩ :  ∀ {S T} → Normal S → Normal T → (S ∩ⁿ T) <: (S ∩ T)
+∩-<:-∩ⁿˢ :  ∀ {S T} → Normal S → Scalar T → (S ∩ T) <: (S ∩ⁿˢ T)
+∩ⁿˢ-<:-∩ :  ∀ {S T} → Normal S → Scalar T → (S ∩ⁿˢ T) <: (S ∩ T)
+∪ᶠ-<:-∪ : ∀ {F G} → FunType F → FunType G → (F ∪ᶠ G) <: (F ∪ G)
+∪ⁿ-<:-∪ : ∀ {S T} → Normal S → Normal T → (S ∪ⁿ T) <: (S ∪ T)
+∪-<:-∪ⁿ : ∀ {S T} → Normal S → Normal T → (S ∪ T) <: (S ∪ⁿ T)
+∪ⁿˢ-<:-∪ : ∀ {S T} → Normal S → OptScalar T → (S ∪ⁿˢ T) <: (S ∪ T)
+∪-<:-∪ⁿˢ : ∀ {S T} → Normal S → OptScalar T → (S ∪ T) <: (S ∪ⁿˢ T)
+
+∩-<:-∩ⁿ S never = <:-∩-right
+∩-<:-∩ⁿ S unknown = <:-∩-left
+∩-<:-∩ⁿ S (T ∪ U) = <:-trans <:-∩-distl-∪ (<:-trans (<:-union (∩-<:-∩ⁿ S T) (∩-<:-∩ⁿˢ S U)) (∪-<:-∪ⁿˢ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) )
+∩-<:-∩ⁿ never (T ⇒ U) = <:-∩-left
+∩-<:-∩ⁿ unknown (T ⇒ U) = <:-∩-right
+∩-<:-∩ⁿ (R ⇒ S) (T ⇒ U) = <:-refl
+∩-<:-∩ⁿ (R ∩ S) (T ⇒ U) = <:-refl
+∩-<:-∩ⁿ (R ∪ S) (T ⇒ U) = <:-trans <:-∩-distr-∪ (<:-trans (<:-union (∩-<:-∩ⁿ R (T ⇒ U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T ⇒ U) S))) (<:-∪-lub <:-refl <:-never))
+∩-<:-∩ⁿ never (T ∩ U) = <:-∩-left
+∩-<:-∩ⁿ unknown (T ∩ U) = <:-∩-right
+∩-<:-∩ⁿ (R ⇒ S) (T ∩ U) = <:-refl
+∩-<:-∩ⁿ (R ∩ S) (T ∩ U) = <:-refl
+∩-<:-∩ⁿ (R ∪ S) (T ∩ U) = <:-trans <:-∩-distr-∪ (<:-trans (<:-union (∩-<:-∩ⁿ R (T ∩ U)) (<:-trans <:-∩-symm (∩-<:-∩ⁿˢ (T ∩ U) S))) (<:-∪-lub <:-refl <:-never))
+
+∩ⁿ-<:-∩ S never = <:-never
+∩ⁿ-<:-∩ S unknown = <:-∩-glb <:-refl <:-unknown
+∩ⁿ-<:-∩ S (T ∪ U) = <:-trans (∪ⁿˢ-<:-∪ (normal-∩ⁿ S T) (normal-∩ⁿˢ S U)) (<:-trans (<:-union (∩ⁿ-<:-∩ S T) (∩ⁿˢ-<:-∩ S U)) ∩-distl-∪-<:)
+∩ⁿ-<:-∩ never (T ⇒ U) = <:-never
+∩ⁿ-<:-∩ unknown (T ⇒ U) = <:-∩-glb <:-unknown <:-refl
+∩ⁿ-<:-∩ (R ⇒ S) (T ⇒ U) = <:-refl
+∩ⁿ-<:-∩ (R ∩ S) (T ⇒ U) = <:-refl
+∩ⁿ-<:-∩ (R ∪ S) (T ⇒ U) = <:-trans (∩ⁿ-<:-∩ R (T ⇒ U)) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right)
+∩ⁿ-<:-∩ never (T ∩ U) = <:-never
+∩ⁿ-<:-∩ unknown (T ∩ U) = <:-∩-glb <:-unknown <:-refl
+∩ⁿ-<:-∩ (R ⇒ S) (T ∩ U) = <:-refl
+∩ⁿ-<:-∩ (R ∩ S) (T ∩ U) = <:-refl
+∩ⁿ-<:-∩ (R ∪ S) (T ∩ U) = <:-trans (∩ⁿ-<:-∩ R (T ∩ U)) (<:-∩-glb (<:-trans <:-∩-left <:-∪-left) <:-∩-right)
+
+∩-<:-∩ⁿˢ never number = <:-∩-left
+∩-<:-∩ⁿˢ never boolean = <:-∩-left
+∩-<:-∩ⁿˢ never string = <:-∩-left
+∩-<:-∩ⁿˢ never nil = <:-∩-left
+∩-<:-∩ⁿˢ unknown T = <:-∩-right
+∩-<:-∩ⁿˢ (R ⇒ S) T = scalar-∩-fun-<:-never (R ⇒ S) T
+∩-<:-∩ⁿˢ (F ∩ G) T = scalar-∩-fun-<:-never (F ∩ G) T
+∩-<:-∩ⁿˢ (R ∪ number) number = <:-∩-right
+∩-<:-∩ⁿˢ (R ∪ boolean) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never boolean number (λ ())))
+∩-<:-∩ⁿˢ (R ∪ string) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never string number (λ ())))
+∩-<:-∩ⁿˢ (R ∪ nil) number = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R number) (scalar-≢-∩-<:-never nil number (λ ())))
+∩-<:-∩ⁿˢ (R ∪ number) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never number boolean (λ ())))
+∩-<:-∩ⁿˢ (R ∪ boolean) boolean = <:-∩-right
+∩-<:-∩ⁿˢ (R ∪ string) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never string boolean (λ ())))
+∩-<:-∩ⁿˢ (R ∪ nil) boolean = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R boolean) (scalar-≢-∩-<:-never nil boolean (λ ())))
+∩-<:-∩ⁿˢ (R ∪ number) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never number string (λ ())))
+∩-<:-∩ⁿˢ (R ∪ boolean) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never boolean string (λ ())))
+∩-<:-∩ⁿˢ (R ∪ string) string = <:-∩-right
+∩-<:-∩ⁿˢ (R ∪ nil) string = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R string) (scalar-≢-∩-<:-never nil string (λ ())))
+∩-<:-∩ⁿˢ (R ∪ number) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never number nil (λ ())))
+∩-<:-∩ⁿˢ (R ∪ boolean) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never boolean nil (λ ())))
+∩-<:-∩ⁿˢ (R ∪ string) nil = <:-trans <:-∩-distr-∪ (<:-∪-lub (∩-<:-∩ⁿˢ R nil) (scalar-≢-∩-<:-never string nil (λ ())))
+∩-<:-∩ⁿˢ (R ∪ nil) nil = <:-∩-right
+
+∩ⁿˢ-<:-∩ never T = <:-never
+∩ⁿˢ-<:-∩ unknown T = <:-∩-glb <:-unknown <:-refl
+∩ⁿˢ-<:-∩ (R ⇒ S) T = <:-never
+∩ⁿˢ-<:-∩ (F ∩ G) T = <:-never
+∩ⁿˢ-<:-∩ (R ∪ number) number = <:-∩-glb <:-∪-right <:-refl
+∩ⁿˢ-<:-∩ (R ∪ boolean) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ string) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ nil) number = <:-trans (∩ⁿˢ-<:-∩ R number) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ number) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ boolean) boolean = <:-∩-glb <:-∪-right <:-refl
+∩ⁿˢ-<:-∩ (R ∪ string) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ nil) boolean = <:-trans (∩ⁿˢ-<:-∩ R boolean) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ number) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ boolean) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ string) string = <:-∩-glb <:-∪-right <:-refl
+∩ⁿˢ-<:-∩ (R ∪ nil) string = <:-trans (∩ⁿˢ-<:-∩ R string) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ number) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ boolean) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ string) nil = <:-trans (∩ⁿˢ-<:-∩ R nil) (<:-intersect <:-∪-left <:-refl)
+∩ⁿˢ-<:-∩ (R ∪ nil) nil = <:-∩-glb <:-∪-right <:-refl
+
+∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U) = <:-trans (<:-function (∩-<:-∩ⁿ R T) (∪ⁿ-<:-∪ S U)) <:-function-∪-∩
+∪ᶠ-<:-∪ (R ⇒ S) (G ∩ H) = <:-trans (<:-intersect (∪ᶠ-<:-∪ (R ⇒ S) G) (∪ᶠ-<:-∪ (R ⇒ S) H)) ∪-distl-∩-<:
+∪ᶠ-<:-∪ (E ∩ F) G = <:-trans (<:-intersect (∪ᶠ-<:-∪ E G) (∪ᶠ-<:-∪ F G)) ∪-distr-∩-<:
+
+∪-<:-∪ᶠ : ∀ {F G} → FunType F → FunType G → (F ∪ G) <: (F ∪ᶠ G)
+∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U) = <:-trans <:-function-∪ (<:-function (∩ⁿ-<:-∩ R T) (∪-<:-∪ⁿ S U))
+∪-<:-∪ᶠ (R ⇒ S) (G ∩ H) = <:-trans <:-∪-distl-∩ (<:-intersect (∪-<:-∪ᶠ (R ⇒ S) G) (∪-<:-∪ᶠ (R ⇒ S) H))
+∪-<:-∪ᶠ (E ∩ F) G = <:-trans <:-∪-distr-∩ (<:-intersect (∪-<:-∪ᶠ E G) (∪-<:-∪ᶠ F G))
+
+∪ⁿˢ-<:-∪ S never = <:-∪-left
+∪ⁿˢ-<:-∪ never number = <:-refl
+∪ⁿˢ-<:-∪ never boolean = <:-refl
+∪ⁿˢ-<:-∪ never string = <:-refl
+∪ⁿˢ-<:-∪ never nil = <:-refl
+∪ⁿˢ-<:-∪ unknown number = <:-∪-left
+∪ⁿˢ-<:-∪ unknown boolean = <:-∪-left
+∪ⁿˢ-<:-∪ unknown string = <:-∪-left
+∪ⁿˢ-<:-∪ unknown nil = <:-∪-left
+∪ⁿˢ-<:-∪ (R ⇒ S) number = <:-refl
+∪ⁿˢ-<:-∪ (R ⇒ S) boolean = <:-refl
+∪ⁿˢ-<:-∪ (R ⇒ S) string = <:-refl
+∪ⁿˢ-<:-∪ (R ⇒ S) nil = <:-refl
+∪ⁿˢ-<:-∪ (R ∩ S) number = <:-refl
+∪ⁿˢ-<:-∪ (R ∩ S) boolean = <:-refl
+∪ⁿˢ-<:-∪ (R ∩ S) string = <:-refl
+∪ⁿˢ-<:-∪ (R ∩ S) nil = <:-refl
+∪ⁿˢ-<:-∪ (R ∪ number) number = <:-union <:-∪-left <:-refl
+∪ⁿˢ-<:-∪ (R ∪ boolean) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ string) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ nil) number = <:-trans (<:-union (∪ⁿˢ-<:-∪ R number) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ number) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ boolean) boolean = <:-union <:-∪-left <:-refl
+∪ⁿˢ-<:-∪ (R ∪ string) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ nil) boolean = <:-trans (<:-union (∪ⁿˢ-<:-∪ R boolean) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ number) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ boolean) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ string) string = <:-union <:-∪-left <:-refl
+∪ⁿˢ-<:-∪ (R ∪ nil) string = <:-trans (<:-union (∪ⁿˢ-<:-∪ R string) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ number) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ boolean) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ string) nil = <:-trans (<:-union (∪ⁿˢ-<:-∪ R nil) <:-refl) flipper
+∪ⁿˢ-<:-∪ (R ∪ nil) nil = <:-union <:-∪-left <:-refl
+
+∪-<:-∪ⁿˢ T never = <:-∪-lub <:-refl <:-never
+∪-<:-∪ⁿˢ never number = <:-refl
+∪-<:-∪ⁿˢ never boolean = <:-refl
+∪-<:-∪ⁿˢ never string = <:-refl
+∪-<:-∪ⁿˢ never nil = <:-refl
+∪-<:-∪ⁿˢ unknown number = <:-unknown
+∪-<:-∪ⁿˢ unknown boolean = <:-unknown
+∪-<:-∪ⁿˢ unknown string = <:-unknown
+∪-<:-∪ⁿˢ unknown nil = <:-unknown
+∪-<:-∪ⁿˢ (R ⇒ S) number = <:-refl
+∪-<:-∪ⁿˢ (R ⇒ S) boolean = <:-refl
+∪-<:-∪ⁿˢ (R ⇒ S) string = <:-refl
+∪-<:-∪ⁿˢ (R ⇒ S) nil = <:-refl
+∪-<:-∪ⁿˢ (R ∩ S) number = <:-refl
+∪-<:-∪ⁿˢ (R ∩ S) boolean = <:-refl
+∪-<:-∪ⁿˢ (R ∩ S) string = <:-refl
+∪-<:-∪ⁿˢ (R ∩ S) nil = <:-refl
+∪-<:-∪ⁿˢ (R ∪ number) number = <:-∪-lub <:-refl <:-∪-right
+∪-<:-∪ⁿˢ (R ∪ boolean) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ string) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ nil) number = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R number) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ number) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ boolean) boolean = <:-∪-lub <:-refl <:-∪-right
+∪-<:-∪ⁿˢ (R ∪ string) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ nil) boolean = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R boolean) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ number) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ boolean) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ string) string = <:-∪-lub <:-refl <:-∪-right
+∪-<:-∪ⁿˢ (R ∪ nil) string = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R string) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ number) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ boolean) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ string) nil = <:-trans flipper (<:-union (∪-<:-∪ⁿˢ R nil) <:-refl)
+∪-<:-∪ⁿˢ (R ∪ nil) nil = <:-∪-lub <:-refl <:-∪-right
+
+∪ⁿ-<:-∪ S never = <:-∪-left
+∪ⁿ-<:-∪ S unknown = <:-∪-right
+∪ⁿ-<:-∪ never (T ⇒ U) = <:-∪-right
+∪ⁿ-<:-∪ unknown (T ⇒ U) = <:-∪-left
+∪ⁿ-<:-∪ (R ⇒ S) (T ⇒ U) = ∪ᶠ-<:-∪ (R ⇒ S) (T ⇒ U)
+∪ⁿ-<:-∪ (R ∩ S) (T ⇒ U) = ∪ᶠ-<:-∪ (R ∩ S) (T ⇒ U)
+∪ⁿ-<:-∪ (R ∪ S) (T ⇒ U) = <:-trans (<:-union (∪ⁿ-<:-∪ R (T ⇒ U)) <:-refl) (<:-∪-lub (<:-∪-lub (<:-trans <:-∪-left <:-∪-left) <:-∪-right) (<:-trans <:-∪-right <:-∪-left))
+∪ⁿ-<:-∪ never (T ∩ U) = <:-∪-right
+∪ⁿ-<:-∪ unknown (T ∩ U) = <:-∪-left
+∪ⁿ-<:-∪ (R ⇒ S) (T ∩ U) = ∪ᶠ-<:-∪ (R ⇒ S) (T ∩ U)
+∪ⁿ-<:-∪ (R ∩ S) (T ∩ U) = ∪ᶠ-<:-∪ (R ∩ S) (T ∩ U)
+∪ⁿ-<:-∪ (R ∪ S) (T ∩ U) = <:-trans (<:-union (∪ⁿ-<:-∪ R (T ∩ U)) <:-refl) (<:-∪-lub (<:-∪-lub (<:-trans <:-∪-left <:-∪-left) <:-∪-right) (<:-trans <:-∪-right <:-∪-left))
+∪ⁿ-<:-∪ S (T ∪ U) = <:-∪-lub (<:-trans (∪ⁿ-<:-∪ S T) (<:-union <:-refl <:-∪-left)) (<:-trans <:-∪-right <:-∪-right)
+
+∪-<:-∪ⁿ S never = <:-∪-lub <:-refl <:-never
+∪-<:-∪ⁿ S unknown = <:-unknown
+∪-<:-∪ⁿ never (T ⇒ U) = <:-∪-lub <:-never <:-refl
+∪-<:-∪ⁿ unknown (T ⇒ U) = <:-unknown
+∪-<:-∪ⁿ (R ⇒ S) (T ⇒ U) = ∪-<:-∪ᶠ (R ⇒ S) (T ⇒ U)
+∪-<:-∪ⁿ (R ∩ S) (T ⇒ U) = ∪-<:-∪ᶠ (R ∩ S) (T ⇒ U)
+∪-<:-∪ⁿ (R ∪ S) (T ⇒ U) =  <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) (<:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ R (T ⇒ U)) <:-refl)))
+∪-<:-∪ⁿ never (T ∩ U) = <:-∪-lub <:-never <:-refl
+∪-<:-∪ⁿ unknown (T ∩ U) = <:-unknown
+∪-<:-∪ⁿ (R ⇒ S) (T ∩ U) = ∪-<:-∪ᶠ (R ⇒ S) (T ∩ U)
+∪-<:-∪ⁿ (R ∩ S) (T ∩ U) = ∪-<:-∪ᶠ (R ∩ S) (T ∩ U)
+∪-<:-∪ⁿ (R ∪ S) (T ∩ U) = <:-trans <:-∪-assocr (<:-trans (<:-union <:-refl <:-∪-symm) (<:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ R (T ∩ U)) <:-refl)))
+∪-<:-∪ⁿ never (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ never T) <:-refl)
+∪-<:-∪ⁿ unknown (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ unknown T) <:-refl)
+∪-<:-∪ⁿ (R ⇒ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ⇒ S) T) <:-refl)
+∪-<:-∪ⁿ (R ∩ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ∩ S) T) <:-refl)
+∪-<:-∪ⁿ (R ∪ S) (T ∪ U) = <:-trans <:-∪-assocl (<:-union (∪-<:-∪ⁿ (R ∪ S) T) <:-refl)
+
+normalize-<: : ∀ T → normalize T <: T
+<:-normalize : ∀ T → T <: normalize T
+
+<:-normalize nil = <:-∪-right
+<:-normalize (S ⇒ T) = <:-function (normalize-<: S) (<:-normalize T)
+<:-normalize never = <:-refl
+<:-normalize unknown = <:-refl
+<:-normalize boolean = <:-∪-right
+<:-normalize number = <:-∪-right
+<:-normalize string = <:-∪-right
+<:-normalize (S ∪ T) = <:-trans (<:-union (<:-normalize S) (<:-normalize T)) (∪-<:-∪ⁿ (normal S) (normal T))
+<:-normalize (S ∩ T) = <:-trans (<:-intersect (<:-normalize S) (<:-normalize T)) (∩-<:-∩ⁿ (normal S) (normal T))
+
+normalize-<: nil = <:-∪-lub <:-never <:-refl
+normalize-<: (S ⇒ T) = <:-function (<:-normalize S) (normalize-<: T)
+normalize-<: never = <:-refl
+normalize-<: unknown = <:-refl
+normalize-<: boolean = <:-∪-lub <:-never <:-refl
+normalize-<: number = <:-∪-lub <:-never <:-refl
+normalize-<: string = <:-∪-lub <:-never <:-refl
+normalize-<: (S ∪ T) = <:-trans (∪ⁿ-<:-∪ (normal S) (normal T)) (<:-union (normalize-<: S) (normalize-<: T))
+normalize-<: (S ∩ T) = <:-trans (∩ⁿ-<:-∩ (normal S) (normal T)) (<:-intersect (normalize-<: S) (normalize-<: T))
+
+