diff --git a/prototyping/Luau/StrictMode.agda b/prototyping/Luau/StrictMode.agda
index 1b028042..d3c0f153 100644
--- 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 _[_]ⱽ)
diff --git a/prototyping/Luau/Type.agda b/prototyping/Luau/Type.agda
index 59d1107f..1d0ec9e5 100644
--- 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)
diff --git a/prototyping/Luau/TypeCheck.agda b/prototyping/Luau/TypeCheck.agda
index cabd27a8..d4fabb90 100644
--- 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)
diff --git a/prototyping/Luau/TypeNormalization.agda b/prototyping/Luau/TypeNormalization.agda
index 8d2f3be5..ba4a00ba 100644
--- a/prototyping/Luau/TypeNormalization.agda
+++ b/prototyping/Luau/TypeNormalization.agda
@@ -1,6 +1,6 @@
 module Luau.TypeNormalization where
 
-open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_; src)
+open import Luau.Type using (Type; nil; number; string; boolean; never; unknown; _⇒_; _∪_; _∩_)
 
 -- The top non-function type
 ¬function : Type
@@ -67,4 +67,3 @@ 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/StrictMode.agda b/prototyping/Properties/StrictMode.agda
index fd2cf2f2..69e9131c 100644
--- 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; +; -; *; /; <; >; <=; >=; ··)
diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda
index 0bd95dd7..5a0f1efd 100644
--- a/prototyping/Properties/Subtyping.agda
+++ b/prototyping/Properties/Subtyping.agda
@@ -6,7 +6,7 @@ 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 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 (_∘_)
@@ -230,8 +230,6 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-function-∪-∩ (function-err s) (function-err (right p)) = right (function-err p)
 
 -- Properties of scalars
-skalar = number ∪ (string ∪ (nil ∪ boolean))
-
 function-≮:-scalar : ∀ {S T U} → (Scalar U) → ((S ⇒ T) ≮: U)
 function-≮:-scalar s = witness function function (scalar-function s)
 
@@ -250,90 +248,12 @@ scalar-≢-impl-≮: s₁ s₂ p = witness (scalar s₁) (scalar s₁) (scalar-s
 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-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)))
-
 skalar-scalar : ∀ {T} (s : Scalar T) → (Language skalar (scalar s))
 skalar-scalar number = left (scalar number)
 skalar-scalar boolean = right (right (right (scalar boolean)))
 skalar-scalar string = right (left (scalar string))
 skalar-scalar nil = right (right (left (scalar nil)))
 
-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)
-
--- 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 ())))
-
--- Properties of src
-¬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 = 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
-
-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
diff --git a/prototyping/Properties/TypeCheck.agda b/prototyping/Properties/TypeCheck.agda
index 0726a4be..37fbeda5 100644
--- 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)