diff --git a/prototyping/Luau/TypeNormalization.agda b/prototyping/Luau/TypeNormalization.agda
new file mode 100644
index 00000000..1a3843e6
--- /dev/null
+++ b/prototyping/Luau/TypeNormalization.agda
@@ -0,0 +1,78 @@
+module Luau.TypeNormalization where
+
+open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src)
+
+-- 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
+_∩ⁿ_ : 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
+
+-- Intersection of function types
+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
+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
+
+-- Functions between normalized types
+(never ⇒ᶠ T) = (never ⇒ unknown)
+(S ⇒ᶠ T) = (S ⇒ 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
+
diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda
index 5594812e..cad6ab07 100644
--- a/prototyping/Properties.agda
+++ b/prototyping/Properties.agda
@@ -11,3 +11,4 @@ import Properties.Step
 import Properties.StrictMode
 import Properties.Subtyping
 import Properties.TypeCheck
+import Properties.TypeNormalization
diff --git a/prototyping/Properties/TypeNormalization.agda b/prototyping/Properties/TypeNormalization.agda
new file mode 100644
index 00000000..84e194a2
--- /dev/null
+++ b/prototyping/Properties/TypeNormalization.agda
@@ -0,0 +1,161 @@
+{-# OPTIONS --rewriting #-}
+
+module Properties.TypeNormalization where
+
+open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src)
+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; ∪-dist-∩-<:; <:-function; <:-function-∪-∩; <:-everything)
+
+-- 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-∩ᶠ : ∀ {F G} → FunType F → FunType G → FunType (F ∩ᶠ G)
+normal-⇒ᶠ : ∀ {S T} → Normal S → Normal T → FunType (S ⇒ᶠ T)
+
+normal nil = never ∪ nil
+normal (S ⇒ T) = normalᶠ (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 = never
+normal-∩ⁿˢ unknown boolean = never
+normal-∩ⁿˢ unknown string = never
+normal-∩ⁿˢ unknown nil = never
+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-⇒ᶠ never T = never ⇒ unknown
+normal-⇒ᶠ unknown T = unknown ⇒ T
+normal-⇒ᶠ (R ⇒ S) T = (R ⇒ S) ⇒ T
+normal-⇒ᶠ (R ∩ S) T = (R ∩ S) ⇒ T
+normal-⇒ᶠ (R ∪ S) T = (R ∪ S) ⇒ T
+
+normal-∩ᶠ F G = F ∩ G
+
+normal-∪ᶠ (R ⇒ S) (T ⇒ U) = normal-⇒ᶠ (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