diff --git a/prototyping/Properties/DecSubtyping.agda b/prototyping/Properties/DecSubtyping.agda
index 503838f9..fdd9a8e5 100644
--- a/prototyping/Properties/DecSubtyping.agda
+++ b/prototyping/Properties/DecSubtyping.agda
@@ -12,22 +12,10 @@ open import Luau.TypeSaturation using (saturate)
 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; <:-impl-¬≮:; <:-intersect; <:-function-∩-∪; <:-function-∩; <:-union; ≮:-left-∪; ≮:-right-∪; <:-∩-distr-∪; <:-impl-⊇; language-comp)
-open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalᶠ; function-top)
+open import Properties.TypeNormalization using (FunType; Normal; never; unknown; _∩_; _∪_; _⇒_; normal; <:-normalize; normalize-<:; normal-∩ⁿ; normal-∪ⁿ; ∪-<:-∪ⁿ; ∪ⁿ-<:-∪; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ; normalᶠ; fun-top; fun-function; fun-¬scalar)
 open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; defn; here; left; right; ov-language; ov-<:; saturated; normal-saturate; normal-overload-src; normal-overload-tgt; saturate-<:; <:-saturate; <:ᵒ-impl-<:; _>>=ˡ_; _>>=ʳ_)
 open import Properties.Equality using (_≢_)
 
-fun-function : ∀ {F} → FunType F → Language F function
-fun-function (S ⇒ T) = function
-fun-function (F ∩ G) = (fun-function F , fun-function G)
-
-fun-¬scalar : ∀ {F S t} → (s : Scalar S) → FunType F → Language F 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-ok₂ p) = scalar-function-ok s
-fun-¬scalar s (S ⇒ T) (function-err p) = scalar-function-err s
-fun-¬scalar s (S ⇒ T) (function-tgt p) = scalar-function-tgt s
-fun-¬scalar s (F ∩ G) (p₁ , p₂) = fun-¬scalar s G p₂
-
 -- Honest this terminates, since saturation maintains the depth of nested arrows
 {-# TERMINATING #-}
 dec-subtypingˢⁿ : ∀ {T U} → Scalar T → Normal U → Either (T ≮: U) (T <: U)
diff --git a/prototyping/Properties/ResolveOverloads.agda b/prototyping/Properties/ResolveOverloads.agda
index a2f30eee..2477ab87 100644
--- a/prototyping/Properties/ResolveOverloads.agda
+++ b/prototyping/Properties/ResolveOverloads.agda
@@ -9,8 +9,8 @@ open import Luau.TypeSaturation using (saturate)
 open import Properties.Contradiction using (CONTRADICTION)
 open import Properties.DecSubtyping using (dec-subtyping; dec-subtypingⁿ; <:-impl-<:ᵒ)
 open import Properties.Functions using (_∘_)
-open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-trans-<:; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∪-right; <:-impl-¬≮:; <:-unknown; <:-function; function-≮:-never; <:-never; unknown-≮:-function; scalar-≮:-function)
-open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize; normalize-<:)
+open import Properties.Subtyping using (<:-refl; <:-trans; <:-trans-≮:; ≮:-trans-<:; <:-∩-left; <:-∩-right; <:-∩-glb; <:-∪-right; <:-impl-¬≮:; <:-unknown; <:-function; function-≮:-never; <:-never; unknown-≮:-function; scalar-≮:-function; ≮:-∪-right; scalar-≮:-never)
+open import Properties.TypeNormalization using (Normal; FunType; normal; _⇒_; _∩_; _∪_; never; unknown; <:-normalize; normalize-<:; fun-≮:-never; unknown-≮:-fun; scalar-≮:-fun)
 open import Properties.TypeSaturation using (Overloads; Saturated; _⊆ᵒ_; _<:ᵒ_; normal-saturate; saturated; <:-saturate; saturate-<:; defn; here; left; right)
 
 data ResolvedTo F G R : Set where
@@ -51,12 +51,12 @@ resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Rⁿ G⊆F | no src₁ | yes S
 resolveˢ (Gᶠ ∩ Hᶠ) (defn sat-∩ sat-∪) Rⁿ G⊆F | no src₁ | no src₂ =
   no (λ { (left o) → src₁ o ; (right o) → src₂ o })
 
-resolveᶠ : ∀ {F R} → FunType F → Normal R → Resolved (saturate F) R
-resolveᶠ Fᶠ Rⁿ = resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Rⁿ (λ o → o)
+resolveᶠ : ∀ {F R} → FunType F → Normal R → Type
+resolveᶠ Fᶠ Rⁿ = target (resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Rⁿ (λ o → o))
 
 resolveⁿ : ∀ {F R} → Normal F → Normal R → Type
-resolveⁿ (Sⁿ ⇒ Tⁿ) Rⁿ = target (resolveᶠ (Sⁿ ⇒ Tⁿ) Rⁿ)
-resolveⁿ (Fᶠ ∩ Gᶠ) Rⁿ = target (resolveᶠ (Fᶠ ∩ Gᶠ) Rⁿ)
+resolveⁿ (Sⁿ ⇒ Tⁿ) Rⁿ = resolveᶠ (Sⁿ ⇒ Tⁿ) Rⁿ
+resolveⁿ (Fᶠ ∩ Gᶠ) Rⁿ = resolveᶠ (Fᶠ ∩ Gᶠ) Rⁿ
 resolveⁿ (Sⁿ ∪ Tˢ) Rⁿ = unknown
 resolveⁿ unknown Rⁿ = unknown
 resolveⁿ never Rⁿ = never
@@ -68,11 +68,11 @@ resolve F R = resolveⁿ (normal F) (normal R)
 <:-target-⇒ (yes Sʳ Tʳ here x₁ x₂) = <:-refl
 <:-target-⇒ (no x) = <:-unknown
 
-<:-resolveⁿ : ∀ {R S T} → (Fⁿ : Normal (S ⇒ T)) → (Rⁿ : Normal R) → T <: resolveⁿ Fⁿ Rⁿ
-<:-resolveⁿ (Sⁿ ⇒ Tⁿ) Rⁿ = <:-target-⇒ (resolveˢ (Sⁿ ⇒ Tⁿ) (saturated (Sⁿ ⇒ Tⁿ)) Rⁿ (λ o → o))
+<:-resolve-⇒ⁿ : ∀ {R S T} → (Fⁿ : Normal (S ⇒ T)) → (Rⁿ : Normal R) → T <: resolveⁿ Fⁿ Rⁿ
+<:-resolve-⇒ⁿ (Sⁿ ⇒ Tⁿ) Rⁿ = <:-target-⇒ (resolveˢ (Sⁿ ⇒ Tⁿ) (saturated (Sⁿ ⇒ Tⁿ)) Rⁿ (λ o → o))
 
-<:-resolve : ∀ {R S T} → T <: resolve (S ⇒ T) R
-<:-resolve {R} {S} {T} = <:-trans (<:-normalize T) (<:-resolveⁿ (normal (S ⇒ T)) (normal R))
+<:-resolve-⇒ : ∀ {R S T} → T <: resolve (S ⇒ T) R
+<:-resolve-⇒ {R} {S} {T} = <:-trans (<:-normalize T) (<:-resolve-⇒ⁿ (normal (S ⇒ T)) (normal R))
 
 resolveˢ-<:-⇒ : ∀ {F R U} → (FunType F) → (Saturated F) → (r : Resolved F R) → (F <: (R ⇒ U)) → (target r <: U)
 resolveˢ-<:-⇒ Fᶠ Fˢ r F<:R⇒U with <:-impl-<:ᵒ Fᶠ Fˢ F<:R⇒U
@@ -93,3 +93,43 @@ resolve-≮:-⇒ : ∀ {F R U} → (resolve F R ≮: U) → (F ≮: (R ⇒ U))
 resolve-≮:-⇒ {F} {R} {U} FR≮:U with dec-subtyping F (R ⇒ U)
 resolve-≮:-⇒ {F} {R} {U} FR≮:U | Left F≮:R⇒U = F≮:R⇒U
 resolve-≮:-⇒ {F} {R} {U} FR≮:U | Right F<:R⇒U = CONTRADICTION (<:-impl-¬≮: (resolve-<:-⇒ F<:R⇒U) FR≮:U)
+
+⇒-<:-resolveⁿ : ∀ {F V U} → (Fⁿ : Normal F) → (Vⁿ : Normal V) → (resolveⁿ Fⁿ Vⁿ <: U) → (F <: (V ⇒ U))
+⇒-<:-resolveⁿ (Sⁿ ⇒ Tⁿ) Vⁿ FV<:U = {!!}
+⇒-<:-resolveⁿ (Fⁿ ∩ Gⁿ) Vⁿ FV<:U = {!!}
+⇒-<:-resolveⁿ (Fⁿ ∪ Tˢ) Vⁿ FV<:U = {!FV<:U!}
+⇒-<:-resolveⁿ never Vⁿ FV<:U = <:-never
+⇒-<:-resolveⁿ unknown Vⁿ FV<:U = {!FV<:U!}
+
+⇒-<:-resolve : ∀ {F V U} → (resolve F V <: U) → (F <: (V ⇒ U))
+⇒-<:-resolve {F} {V} {U} FV<:U = {!!}
+
+⇒-≮:-resolve : ∀ {F V U} → (F ≮: (V ⇒ U)) → (resolve F V ≮: U)
+⇒-≮:-resolve F≮:V⇒U = {!!}
+
+<:-resolveˢ : ∀ {F G V W} → (r : Resolved F V) → (s : Resolved G W) → (F <: G) → (V <: W) → target r <: target s
+<:-resolveˢ = {!!}
+
+<:-resolveᶠ : ∀ {F G V W} → (Fᶠ : FunType F) → (Gᶠ : FunType G) → (Vⁿ : Normal V) → (Wⁿ : Normal W) → (F <: G) → (V <: W) → resolveᶠ Fᶠ Vⁿ <: resolveᶠ Gᶠ Wⁿ
+<:-resolveᶠ Fᶠ Gᶠ Vⁿ Wⁿ F<:G V<:W = <:-resolveˢ (resolveˢ (normal-saturate Fᶠ) (saturated Fᶠ) Vⁿ (λ o → o)) (resolveˢ (normal-saturate Gᶠ) (saturated Gᶠ) Wⁿ (λ o → o)) (<:-trans (saturate-<: Fᶠ) (<:-trans F<:G (<:-saturate Gᶠ))) V<:W
+
+<:-resolveⁿ : ∀ {F G V W} → (Fⁿ : Normal F) → (Gⁿ : Normal G) → (Vⁿ : Normal V) → (Wⁿ : Normal W) → (F <: G) → (V <: W) → resolveⁿ Fⁿ Vⁿ <: resolveⁿ Gⁿ Wⁿ
+<:-resolveⁿ (Rⁿ ⇒ Sⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Rⁿ ⇒ Sⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W
+<:-resolveⁿ (Rⁿ ⇒ Sⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Rⁿ ⇒ Sⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W
+<:-resolveⁿ (Eⁿ ∩ Fⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Eⁿ ∩ Fⁿ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W
+<:-resolveⁿ (Eⁿ ∩ Fⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = <:-resolveᶠ (Eⁿ ∩ Fⁿ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W
+<:-resolveⁿ (Fⁿ ∪ Sˢ) (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (≮:-∪-right (scalar-≮:-function Sˢ)))
+<:-resolveⁿ unknown (Tⁿ ⇒ Uⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G unknown-≮:-function)
+<:-resolveⁿ (Fⁿ ∪ Sˢ) (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (≮:-∪-right (scalar-≮:-fun (Gⁿ ∩ Hⁿ) Sˢ)))
+<:-resolveⁿ unknown (Gⁿ ∩ Hⁿ) Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (unknown-≮:-fun (Gⁿ ∩ Hⁿ)))
+<:-resolveⁿ (Rⁿ ⇒ Sⁿ) never Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (fun-≮:-never (Rⁿ ⇒ Sⁿ)))
+<:-resolveⁿ (Eⁿ ∩ Fⁿ) never Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (fun-≮:-never (Eⁿ ∩ Fⁿ)))
+<:-resolveⁿ (Fⁿ ∪ Sˢ) never Vⁿ Wⁿ F<:G V<:W = CONTRADICTION (<:-impl-¬≮: F<:G (≮:-∪-right (scalar-≮:-never Sˢ)))
+<:-resolveⁿ unknown never Vⁿ Wⁿ F<:G V<:W = F<:G
+<:-resolveⁿ never Gⁿ Vⁿ Wⁿ F<:G V<:W = <:-never
+<:-resolveⁿ Fⁿ (Gⁿ ∪ Uˢ) Vⁿ Wⁿ F<:G V<:W = <:-unknown
+<:-resolveⁿ Fⁿ unknown Vⁿ Wⁿ F<:G V<:W = <:-unknown
+
+<:-resolve : ∀ {F G V W} → (F <: G) → (V <: W) → resolve F V <: resolve G W
+<:-resolve F<:G V<:W = {!!}
+
diff --git a/prototyping/Properties/TypeNormalization.agda b/prototyping/Properties/TypeNormalization.agda
index 49f6df22..cbd8139f 100644
--- a/prototyping/Properties/TypeNormalization.agda
+++ b/prototyping/Properties/TypeNormalization.agda
@@ -3,7 +3,7 @@
 module Properties.TypeNormalization where
 
 open import Luau.Type using (Type; Scalar; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
-open import Luau.Subtyping using (Tree; Language; function; scalar; unknown; right; scalar-function-err; _,_)
+open import Luau.Subtyping using (Tree; Language; ¬Language; function; scalar; unknown; left; right; function-ok₁; function-ok₂; function-err; function-tgt; scalar-function; scalar-function-ok; scalar-function-err; scalar-function-tgt; function-scalar; _,_)
 open import Luau.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; normalize)
 open import Luau.Subtyping using (_<:_; _≮:_; witness; never)
 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)
@@ -31,9 +31,36 @@ data OptScalar : Type → Set where
   nil : OptScalar nil
 
 -- Top function type
-function-top : ∀ {F} → (FunType F) → (F <: (never ⇒ unknown))
-function-top (S ⇒ T) = <:-function <:-never <:-unknown
-function-top (F ∩ G) = <:-trans <:-∩-left (function-top F)
+fun-top : ∀ {F} → (FunType F) → (F <: (never ⇒ unknown))
+fun-top (S ⇒ T) = <:-function <:-never <:-unknown
+fun-top (F ∩ G) = <:-trans <:-∩-left (fun-top F)
+
+-- function types are inhabited
+fun-function : ∀ {F} → FunType F → Language F function
+fun-function (S ⇒ T) = function
+fun-function (F ∩ G) = (fun-function F , fun-function G)
+
+fun-≮:-never : ∀ {F} → FunType F → (F ≮: never)
+fun-≮:-never F = witness function (fun-function F) never
+
+-- function types aren't scalars
+fun-¬scalar : ∀ {F S t} → (s : Scalar S) → FunType F → Language F 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-ok₂ p) = scalar-function-ok s
+fun-¬scalar s (S ⇒ T) (function-err p) = scalar-function-err s
+fun-¬scalar s (S ⇒ T) (function-tgt p) = scalar-function-tgt s
+fun-¬scalar s (F ∩ G) (p₁ , p₂) = fun-¬scalar s G p₂
+
+¬scalar-fun : ∀ {F S} → FunType F → (s : Scalar S) → ¬Language F (scalar s)
+¬scalar-fun (S ⇒ T) s = function-scalar s
+¬scalar-fun (F ∩ G) s = left (¬scalar-fun F s)
+
+scalar-≮:-fun : ∀ {F S} → FunType F → Scalar S → S ≮: F
+scalar-≮:-fun F s = witness (scalar s) (scalar s) (¬scalar-fun F s)
+
+unknown-≮:-fun : ∀ {F} → FunType F → unknown ≮: F
+unknown-≮:-fun F = witness (scalar nil) unknown (¬scalar-fun F nil)
 
 -- Normalization produces normal types
 normal : ∀ T → Normal (normalize T)
diff --git a/prototyping/Properties/TypeSaturation.agda b/prototyping/Properties/TypeSaturation.agda
index b5bc068c..4e817bf7 100644
--- a/prototyping/Properties/TypeSaturation.agda
+++ b/prototyping/Properties/TypeSaturation.agda
@@ -9,7 +9,7 @@ open import Luau.Type using (Type; _⇒_; _∩_; _∪_; never; unknown)
 open import Luau.TypeNormalization using (_∩ⁿ_; _∪ⁿ_)
 open import Luau.TypeSaturation using (_⋓_; _⋒_; _∩ᵘ_; _∩ⁱ_; ∪-saturate; ∩-saturate; saturate)
 open import Properties.Subtyping using (dec-language; language-comp; <:-impl-⊇; <:-refl; <:-trans; <:-trans-≮:; <:-impl-¬≮: ; <:-never; <:-unknown; <:-function; <:-union; <:-∪-symm; <:-∪-left; <:-∪-right; <:-∪-lub; <:-∪-assocl; <:-∪-assocr; <:-intersect; <:-∩-symm; <:-∩-left; <:-∩-right; <:-∩-glb; ≮:-function-left; ≮:-function-right; <:-function-∩-∪; <:-function-∩-∩; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:)
-open import Properties.TypeNormalization using (Normal; FunType; _⇒_; _∩_; _∪_; never; unknown; function-top; normal-∪ⁿ; normal-∩ⁿ; ∪ⁿ-<:-∪; ∪-<:-∪ⁿ; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ)
+open import Properties.TypeNormalization using (Normal; FunType; _⇒_; _∩_; _∪_; never; unknown; normal-∪ⁿ; normal-∩ⁿ; ∪ⁿ-<:-∪; ∪-<:-∪ⁿ; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ)
 open import Properties.Contradiction using (CONTRADICTION)
 open import Properties.Functions using (_∘_)