diff --git a/prototyping/Luau/OverloadedFunctions.agda b/prototyping/Luau/OverloadedFunctions.agda
index 69620450..c9167e08 100644
--- a/prototyping/Luau/OverloadedFunctions.agda
+++ b/prototyping/Luau/OverloadedFunctions.agda
@@ -2,7 +2,7 @@
 
 open import FFI.Data.Either using (Either; Left; Right)
 open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src)
-open import Properties.Subtyping using (dec-subtyping)
+open import Properties.DecSubtyping using (dec-subtyping)
 
 module Luau.OverloadedFunctions where
 
diff --git a/prototyping/Properties.agda b/prototyping/Properties.agda
index 5594812e..154e90c9 100644
--- a/prototyping/Properties.agda
+++ b/prototyping/Properties.agda
@@ -6,6 +6,7 @@ import Properties.Contradiction
 import Properties.Dec
 import Properties.Equality
 import Properties.Functions
+import Properties.OverloadedFunctions
 import Properties.Remember
 import Properties.Step
 import Properties.StrictMode
diff --git a/prototyping/Properties/OverloadedFunctions.agda b/prototyping/Properties/OverloadedFunctions.agda
index b8c0efb2..2ba21e80 100644
--- a/prototyping/Properties/OverloadedFunctions.agda
+++ b/prototyping/Properties/OverloadedFunctions.agda
@@ -6,7 +6,9 @@ open import FFI.Data.Either using (Either; Left; Right)
 open import Luau.OverloadedFunctions using (resolve)
 open import Luau.Subtyping using (_<:_; _≮:_)
 open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src)
-open import Properties.Subtyping using (dec-subtyping)
+open import Properties.Contradiction using (CONTRADICTION)
+open import Properties.DecSubtyping using (dec-subtyping)
+open import Properties.Subtyping using (<:-refl; <:-trans; <:-union; <:-∪-left; <:-∪-right; <:-∪-lub; <:-intersect; <:-∩-left; <:-∩-right; <:-∩-glb; <:-impl-¬≮:; <:-function; <:-never; <:-never-left; <:-never-right; <:-function-∩; <:-function-∩-∪; <:-∩-dist-∪)
 
 -- Function overload resolution respects subtyping
 
@@ -18,9 +20,9 @@ resolve-<: unknown p = <:-refl
 resolve-<: boolean p = <:-refl
 resolve-<: number p = <:-refl
 resolve-<: string p = <:-refl
-resolve-<: (F ∪ G) p = ∪-<: (resolve-<: F p) (resolve-<: G p)
+resolve-<: (F ∪ G) p = <:-union (resolve-<: F p) (resolve-<: G p)
 resolve-<: (F ∩ G) {S} {T} p with dec-subtyping S (src F) | dec-subtyping S (src G) | dec-subtyping T (src F) | dec-subtyping T (src G)
-resolve-<: (F ∩ G) {S} {T} p | Left q₁  | Left q₂  | Left q₃  | Left q₄  = ∪-<: (resolve-<: F p) (resolve-<: G p)
+resolve-<: (F ∩ G) {S} {T} p | Left q₁  | Left q₂  | Left q₃  | Left q₄  = <:-union (resolve-<: F p) (resolve-<: G p)
 resolve-<: (F ∩ G) {S} {T} p | _        | Left q₂  | _        | Right q₄ = CONTRADICTION (<:-impl-¬≮: (<:-trans p q₄) q₂)
 resolve-<: (F ∩ G) {S} {T} p | Left q₁  | _        | Right q₃ | _        = CONTRADICTION (<:-impl-¬≮: (<:-trans p q₃) q₁)
 resolve-<: (F ∩ G) {S} {T} p | Left q₁  | Right q₂ | Left q₃  | Left q₄  = <:-trans (resolve-<: G p) <:-∪-right
@@ -30,20 +32,20 @@ resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Left q₂  | Right q₃ | Left q
 resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Right q₂ | Left q₃  | Left q₄  = <:-trans <:-∩-left (<:-trans (resolve-<: F p) <:-∪-left)
 resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Right q₂ | Left q₃  | Right q₄ = <:-trans <:-∩-right (resolve-<: G p)
 resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Right q₂ | Right q₃ | Left q₄  = <:-trans <:-∩-left (resolve-<: F p)
-resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Right q₂ | Right q₃ | Right q₄ = ∩-<: (resolve-<: F p) (resolve-<: G p)
+resolve-<: (F ∩ G) {S} {T} p | Right q₁ | Right q₂ | Right q₃ | Right q₄ = <:-intersect (resolve-<: F p) (resolve-<: G p)
 
 -- A function type is a subtype of any of its overloadings
 resolve-intro : ∀ F V → (V ≮: never) → (V <: src F) → F <: (V ⇒ resolve F V)
 resolve-intro nil V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁)
-resolve-intro (S ⇒ T) V p₁ p₂ = function-<: p₂ <:-refl
+resolve-intro (S ⇒ T) V p₁ p₂ = <:-function p₂ <:-refl
 resolve-intro never V p₁ p₂ = <:-never
 resolve-intro unknown V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁)
 resolve-intro boolean V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁)
 resolve-intro number V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁)
 resolve-intro string V p₁ p₂ = CONTRADICTION (<:-impl-¬≮: p₂ p₁)
-resolve-intro (F ∪ G) V p₁ p₂ = <:-∪-lub (<:-trans (resolve-intro F V p₁ (<:-trans p₂ <:-∩-left)) (function-<: <:-refl <:-∪-left)) (<:-trans (resolve-intro G V p₁ (<:-trans p₂ <:-∩-right)) (function-<: <:-refl <:-∪-right))
+resolve-intro (F ∪ G) V p₁ p₂ = <:-∪-lub (<:-trans (resolve-intro F V p₁ (<:-trans p₂ <:-∩-left)) (<:-function <:-refl <:-∪-left)) (<:-trans (resolve-intro G V p₁ (<:-trans p₂ <:-∩-right)) (<:-function <:-refl <:-∪-right))
 resolve-intro (F ∩ G) V p₁ p₂ with dec-subtyping V (src F) | dec-subtyping V (src G)
-resolve-intro (F ∩ G) V p₁ p₂ | Left q₁ | Left q₂ = <:-trans (∩-<: (resolve-intro F (V ∩ src F) (<:-never-right p₂ q₂) <:-∩-right) ((resolve-intro G (V ∩ src G) (<:-never-left p₂ q₁) <:-∩-right))) (<:-trans function-∩-∪-<: (function-<: (<:-trans (<:-∩-glb <:-refl p₂) <:-∩-dist-∪) (∪-<: (resolve-<: F <:-∩-left) (resolve-<: G <:-∩-left))))
+resolve-intro (F ∩ G) V p₁ p₂ | Left q₁ | Left q₂ = <:-trans (<:-intersect (resolve-intro F (V ∩ src F) (<:-never-right p₂ q₂) <:-∩-right) ((resolve-intro G (V ∩ src G) (<:-never-left p₂ q₁) <:-∩-right))) (<:-trans <:-function-∩-∪ (<:-function (<:-trans (<:-∩-glb <:-refl p₂) <:-∩-dist-∪) (<:-union (resolve-<: F <:-∩-left) (resolve-<: G <:-∩-left))))
 resolve-intro (F ∩ G) V p₁ p₂ | Left q₁ | Right q₂ = <:-trans <:-∩-right (resolve-intro G V p₁ q₂)
 resolve-intro (F ∩ G) V p₁ p₂ | Right q₁ | Left q₂ = <:-trans <:-∩-left (resolve-intro F V p₁ q₁)
-resolve-intro (F ∩ G) V p₁ p₂ | Right q₁ | Right q₂ = <:-trans (∩-<: (resolve-intro F V p₁ q₁) (resolve-intro G V p₁ q₂)) function-∩-<:
+resolve-intro (F ∩ G) V p₁ p₂ | Right q₁ | Right q₂ = <:-trans (<:-intersect (resolve-intro F V p₁ q₁) (resolve-intro G V p₁ q₂)) <:-function-∩
diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda
index c7303d9b..b628adf5 100644
--- a/prototyping/Properties/Subtyping.agda
+++ b/prototyping/Properties/Subtyping.agda
@@ -8,7 +8,7 @@ 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-ok₁; 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 Properties.DecSubtyping using (language-comp; dec-language; function-err-src; ¬function-err-src; src-¬function-err)
+open import Properties.DecSubtyping using (language-comp; dec-language; function-err-src; ¬function-err-src; src-¬function-err; <:-impl-⊇)
 open import Properties.Equality using (_≢_)
 open import Properties.Functions using (_∘_)
 open import Properties.Product using (_×_; _,_)
@@ -42,6 +42,61 @@ open import Properties.Product using (_×_; _,_)
 <:-trans : ∀ {S T U} → (S <: T) → (T <: U) → (S <: U)
 <:-trans p q = ¬≮:-impl-<: (cond (<:-impl-¬≮: p) (<:-impl-¬≮: q) ∘ ≮:-trans)
 
+-- 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
+
+-- 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)
+
+<:-∩-dist-∪ : ∀ {S T U} → (S ∩ (T ∪ U)) <: ((S ∩ T) ∪ (S ∩ U))
+<:-∩-dist-∪ t (p₁ , left p₂) = left (p₁ , p₂)
+<:-∩-dist-∪ t (p₁ , right p₂) = right (p₁ , 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 s t) (function-ok₁ r) = function-ok₁ (<:-impl-⊇ p s r)
+<:-function p q (function-ok s 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 s t) (function-ok₁ p₁ , function-ok₁ p₂) = function-ok₁ (p₁ , p₂)
+<:-function-∩-∪ (function-ok s t) (p₁ , function-ok₂ p₂) = function-ok₂ (right p₂)
+<:-function-∩-∪ (function-ok _ _) (function-ok₂ p₁ , p₂) = function-ok₂ (left 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 s t) (p₁ , function-ok₁ p₂) = function-ok₁ p₂
+<:-function-∩ (function-ok s t) (function-ok₁ p₁ , p₂) = function-ok₁ p₁
+<:-function-∩ (function-ok s t) (function-ok₂ p₁ , function-ok₂ p₂) = function-ok₂ (p₁ , p₂)
+<:-function-∩ (function-err s) (function-err p₁ , function-err p₂) = function-err p₂
+
 -- Properties of scalars
 skalar = number ∪ (string ∪ (nil ∪ boolean))
 
@@ -101,6 +156,20 @@ 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 t (scalar-function-err ())
+
+<:-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)
+
 -- 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,