WIP

prototyping/Properties/Subtyping.agda

@@ -263,6 +263,17 @@ language-comp (function-err t) (function-err p) (function-err q) = language-comp
 <:-function-never (function-ok s t) (function-ok₂ p) = function-ok₁ never
 <:-function-never (function-err s) (function-err p) = function-err p
 
+<:-function-left : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (R <: S)
+<:-function-left {R} {S} p s Rs with dec-language S s
+<:-function-left p s Rs | Right Ss = Ss
+<:-function-left p s Rs | Left ¬Ss with p (function-err s) (function-err ¬Ss)
+<:-function-left p s Rs | Left ¬Ss | function-err ¬Rs = CONTRADICTION (language-comp s ¬Rs Rs)
+
+<:-function-right : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (R ≮: never) → (T <: U)
+<:-function-right p (witness s Rs never) t Tt with p (function-ok s t) (function-ok₂ Tt)
+<:-function-right p (witness s Rs never) t Tt | function-ok₁ ¬Rs = CONTRADICTION (language-comp s ¬Rs Rs)
+<:-function-right p (witness s Rs never) t Tt | function-ok₂ St = St
+
 ≮:-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)
 

prototyping/Properties/TypeNormalization.agda

@@ -5,7 +5,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.TypeNormalization using (_∪ⁿ_; _∩ⁿ_; _∪ᶠ_; _∪ⁿˢ_; _∩ⁿˢ_; _⇒ⁿ_; tgtⁿ; normalize)
-open import Luau.Subtyping using (_<:_)
+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; <:-function-never)
 
 -- Normal forms for types
@@ -61,6 +61,9 @@ inhabited (S ∩ T) = inhabitedᶠ (S ∩ T)
 inhabited (S ∪ T) = right (scalar T)
 inhabited unknown = unknown
 
+inhabited-≮:-never : ∀ {T} → (Inhabited T) → (T ≮: never)
+inhabited-≮:-never Tⁱ = witness (inhabitant Tⁱ) (inhabited Tⁱ) never
+
 -- Top function type
 function-top : ∀ {F} → (FunType F) → (F <: (never ⇒ unknown))
 function-top function = <:-refl

prototyping/Properties/TypeSaturation.agda

@@ -8,45 +8,11 @@ open import Luau.Subtyping using (Tree; Language; ¬Language; _<:_; _≮:_; witn
 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; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:)
+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-never; <:-∩-assocl; <:-∩-assocr; ∩-<:-∪; <:-∩-distl-∪; ∩-distl-∪-<:; <:-∩-distr-∪; ∩-distr-∪-<:)
 open import Properties.TypeNormalization using (FunType; function; _⇒_; _∩_; _∪_; never; unknown; inhabitant; inhabited; function-top; normal-⇒ⁿ; normal-∪ⁿ; normal-∩ⁿ; normalⁱ; <:-tgtⁿ; ∪ⁿ-<:-∪; ∪-<:-∪ⁿ; ∩ⁿ-<:-∩; ∩-<:-∩ⁿ)
 open import Properties.Contradiction using (CONTRADICTION)
 open import Properties.Functions using (_∘_)
 
--- Overload F (S ⇒ T) when (S ⇒ T) is an overload of F
-data Overload : Type → Type → Set where
-
-   here : ∀ {S T} → Overload (S ⇒ T) (S ⇒ T)
-   left : ∀ {S T F G} → Overload F (S ⇒ T) → Overload (F ∩ G) (S ⇒ T)
-   right : ∀ {S T F G} → Overload G (S ⇒ T) → Overload (F ∩ G) (S ⇒ T)
-
--- F <:ᵒ (S ⇒ T) when (S ⇒ T) is a supertype of an overload of F
-data _<:ᵒ_ : Type → Type → Set where
-
-  defn : ∀ {F R S T U} →
-
-    Overload F (R ⇒ S) →
-    T <: R →
-    S <: U →
-    ---------------------
-    F <:ᵒ (T ⇒ U)
-
--- Saturated F whenever
--- * if F has overloads (R ⇒ S) and (T ⇒ U) then F has an overload which is a subtype of ((R ∩ T) ⇒ (S ∩ U))
--- * ditto union
-
-data Saturated (F : Type) : Set where
-
-  defn : 
-
-    (∀ {R S T U} → Overload F (R ⇒ S) → Overload F (T ⇒ U) → F <:ᵒ ((R ∩ T) ⇒ (S ∩ U))) →
-    (∀ {R S T U} → Overload F (R ⇒ S) → Overload F (T ⇒ U) → F <:ᵒ ((R ∪ T) ⇒ (S ∪ U))) →
-    -----------
-    Saturated F
-
--- Saturated functions are interesting because they have a decision procedure
--- for subtyping.
-
 -- Saturation preserves normalization
 normal-⋒ : ∀ {F G} → FunType F → FunType G → FunType (F ⋒ G)
 normal-⋒ function function = function
@@ -79,356 +45,343 @@ normal-∪-saturate (F ∩ G) = (normal-∪-saturate F ∩ normal-∪-saturate G
 normal-saturate : ∀ {F} → FunType F → FunType (saturate F)
 normal-saturate F = normal-∪-saturate (normal-∩-saturate F)
 
--- Order types by overloading
+-- Overloads F is the set of overloads of F (including never ⇒ never).
+data Overloads : Type → Type → Set where
+
+   never : ∀ {F} → Overloads F (never ⇒ never)
+   here : ∀ {S T} → Overloads (S ⇒ T) (S ⇒ T)
+   left : ∀ {S T F G} → Overloads F (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T)
+   right : ∀ {S T F G} → Overloads G (S ⇒ T) → Overloads (F ∩ G) (S ⇒ T)
+
+-- An inductive presentation of the overloads of F ⋓ G
+data ∪-Lift (P Q : Type → Set) : Type → Set where
+
+  union : ∀ {R S T U} →
+
+    P (R ⇒ S) →
+    Q (T ⇒ U) →
+    --------------------
+    ∪-Lift P Q ((R ∪ T) ⇒ (S ∪ U))
+
+-- An inductive presentation of the overloads of F ⋒ G
+data ∩-Lift (P Q : Type → Set) : Type → Set where
+
+  intersect : ∀ {R S T U} →
+
+    P (R ⇒ S) →
+    Q (T ⇒ U) →
+    --------------------
+    ∩-Lift P Q ((R ∩ T) ⇒ (S ∩ U))
+
+-- An inductive presentation of the overloads of ∪-saturate F
+data ∪-Saturate (P : Type → Set) : Type → Set where
+
+  base : ∀ {S T} →
+
+    P (S ⇒ T) →
+    --------------------
+    ∪-Saturate P (S ⇒ T)
+
+  union : ∀ {R S T U} →
+
+    ∪-Saturate P (R ⇒ S) →
+    ∪-Saturate P (T ⇒ U) →
+    --------------------
+    ∪-Saturate P ((R ∪ T) ⇒ (S ∪ U))
+
+-- An inductive presentation of the overloads of ∩-saturate F
+data ∩-Saturate (P : Type → Set) : Type → Set where
+
+  base : ∀ {S T} →
+
+    P (S ⇒ T) →
+    --------------------
+    ∩-Saturate P (S ⇒ T)
+
+  intersect : ∀ {R S T U} →
+
+    ∩-Saturate P (R ⇒ S) →
+    ∩-Saturate P (T ⇒ U) →
+    --------------------
+    ∩-Saturate P ((R ∩ T) ⇒ (S ∩ U))
+
+-- The <:-up-closure of a set of function types
+data <:-Close (P : Type → Set) : Type → Set where
+
+  defn : ∀ {R S T U} →
+
+    P (S ⇒ T) →
+    R <: S →
+    T <: U →
+    ------------------
+    <:-Close P (R ⇒ U)
+
 -- F ⊆ᵒ G whenever every overload of F is an overload of G
 _⊆ᵒ_ : Type → Type → Set
-F ⊆ᵒ G = ∀ {S T} → Overload F (S ⇒ T) → Overload G (S ⇒ T)
+F ⊆ᵒ G = ∀ {S T} → Overloads F (S ⇒ T) → Overloads G (S ⇒ T)
 
--- F ⊂:ᵒ G whenever every overload of F is a subtype of an overload of G
+-- P ⊂: Q when any type in P is a subtype of some type in Q
-_⊂:ᵒ_ : Type → Type → Set
+_⊂:_ : (Type → Set) → (Type → Set) → Set
-F ⊂:ᵒ G = ∀ {S T} → Overload F (S ⇒ T) → G <:ᵒ (S ⇒ T)
+P ⊂: Q = ∀ {S T} → P (S ⇒ T) → <:-Close Q (S ⇒ T)
 
--- Properties of <:ᵒ
+-- <:-Close is a monad
-⋒-⋓-cl-impl-sat : ∀ {F} → (F ⋒ F) ⊂:ᵒ F → (F ⋓ F) ⊂:ᵒ F → Saturated F
+just : ∀ {P S T} → P (S ⇒ T) → <:-Close P (S ⇒ T)
-⋒-⋓-cl-impl-sat = {!!}
+just p = {!!}
 
-<:ᵒ-refl : ∀ {S T} → (S ⇒ T) <:ᵒ (S ⇒ T)
+infixl 5 _>>=_ _>>=ˡ_ _>>=ʳ_
-<:ᵒ-refl = defn here <:-refl <:-refl
+_>>=_ : ∀ {P Q S T} → <:-Close P (S ⇒ T) → (P ⊂: Q) → <:-Close Q (S ⇒ T)
+p >>= P⊂Q = {!!}
 
-<:ᵒ-left : ∀ {F G S T} → F <:ᵒ (S ⇒ T) → (F ∩ G) <:ᵒ (S ⇒ T)
+_>>=ˡ_ : ∀ {P R S T} → <:-Close P (S ⇒ T) → (R <: S) → <:-Close P (R ⇒ T)
-<:ᵒ-left = {!!}
+_>>=ˡ_ = {!!}
 
-<:ᵒ-right : ∀ {F G S T} → G <:ᵒ (S ⇒ T) → (F ∩ G) <:ᵒ (S ⇒ T)
+_>>=ʳ_ : ∀ {P S T U} → <:-Close P (S ⇒ T) → (T <: U) → <:-Close P (S ⇒ U)
-<:ᵒ-right = {!!}
+_>>=ʳ_ = {!!}
 
-<:ᵒ-ov : ∀ {F S T} → Overload F (S ⇒ T) → F <:ᵒ (S ⇒ T)
+-- F <:ᵒ (S ⇒ T) when (S ⇒ T) is a supertype of an overload of F
-<:ᵒ-ov o = defn o <:-refl <:-refl
+_<:ᵒ_ : Type → Type → Set
+_<:ᵒ_ F = <:-Close (Overloads F)
 
-<:ᵒ-trans-<: : ∀ {F S T S′ T′} → F <:ᵒ (S ⇒ T) → (S′ <: S) → (T <: T′) → F <:ᵒ (S′ ⇒ T′)
+⊂:-∩-saturate-inj : ∀ {P} → P ⊂: ∩-Saturate P
-<:ᵒ-trans-<: = {!!}
+⊂:-∩-saturate-inj p = defn (base p) <:-refl <:-refl
 
-ov-language : ∀ {F t} → FunType F → (∀ {S T} → Overload F (S ⇒ T) → Language (S ⇒ T) t) → Language F t
+⊂:-∩-saturate-indn : ∀ {P Q} → (P ⊂: Q) → (∩-Lift Q Q ⊂: Q) → (∩-Saturate P ⊂: Q)
+⊂:-∩-saturate-indn = {!!}
+
+⊂:-∩-saturate : ∀ {P Q} → (P ⊂: Q) → (∩-Saturate P ⊂: ∩-Saturate Q)
+⊂:-∩-saturate P⊂Q p = {!!}
+
+⊂:-∪-saturate-inj : ∀ {P} → P ⊂: ∪-Saturate P
+⊂:-∪-saturate-inj p = defn (base p) (λ t z → z) (λ t z → z)
+
+⊂:-∪-saturate : ∀ {P Q} → (P ⊂: Q) → (∪-Saturate P ⊂: ∪-Saturate Q)
+⊂:-∪-saturate P⊂Q p = {!!}
+
+_[∪]_ : ∀ {P Q R S T U} → <:-Close P (R ⇒ S) → <:-Close Q (T ⇒ U) → <:-Close (∪-Lift P Q) ((R ∪ T) ⇒ (S ∪ U))
+p [∪] q = {!!}
+
+_[∩]_ : ∀ {P Q R S T U} → <:-Close P (R ⇒ S) → <:-Close Q (T ⇒ U) → <:-Close (∩-Lift P Q) ((R ∩ T) ⇒ (S ∩ U))
+p [∩] q = {!!}
+
+⊂:-∩-saturate-lift : ∀ {P} → (∪-Lift P P ⊂: P) → (∪-Saturate P ⊂: P)
+⊂:-∩-saturate-lift ∪P⊂P (base p) = defn p <:-refl <:-refl
+⊂:-∩-saturate-lift ∪P⊂P (union p q) = (⊂:-∩-saturate-lift ∪P⊂P p [∪] ⊂:-∩-saturate-lift ∪P⊂P q) >>= ∪P⊂P
+
+⊂:-∩-lift-saturate : ∀ {P} → ∩-Lift (∩-Saturate P) (∩-Saturate P) ⊂: ∩-Saturate P
+⊂:-∩-lift-saturate (intersect p q) = defn (intersect p q) <:-refl <:-refl
+
+⊂:-∪-lift-saturate : ∀ {P} → ∪-Lift (∪-Saturate P) (∪-Saturate P) ⊂: ∪-Saturate P
+⊂:-∪-lift-saturate = {!!}
+
+∪-saturate-resp-∩-saturation : ∀ {P} → (∩-Lift P P ⊂: P) → (∩-Lift (∪-Saturate P) (∪-Saturate P) ⊂: ∪-Saturate P)
+∪-saturate-resp-∩-saturation ∩P⊂P (intersect (base p) (base q)) = ∩P⊂P (intersect p q) >>= ⊂:-∪-saturate-inj
+∪-saturate-resp-∩-saturation ∩P⊂P (intersect p (union q q₁)) = (∪-saturate-resp-∩-saturation ∩P⊂P (intersect p q) [∪] ∪-saturate-resp-∩-saturation ∩P⊂P (intersect p q₁)) >>= ⊂:-∪-lift-saturate >>=ˡ <:-∩-distl-∪ >>=ʳ ∩-distl-∪-<:
+∪-saturate-resp-∩-saturation ∩P⊂P (intersect (union p p₁) q) = (∪-saturate-resp-∩-saturation ∩P⊂P (intersect p q) [∪] ∪-saturate-resp-∩-saturation ∩P⊂P (intersect p₁ q)) >>= ⊂:-∪-lift-saturate >>=ˡ <:-∩-distr-∪ >>=ʳ ∩-distr-∪-<:
+
+ov-language : ∀ {F t} → FunType F → (∀ {S T} → Overloads F (S ⇒ T) → Language (S ⇒ T) t) → Language F t
 ov-language function p = p here
 ov-language (S ⇒ T) p = p here
 ov-language (F ∩ G) p = (ov-language F (p ∘ left) , ov-language G (p ∘ right))
 
-ov-<: : ∀ {F R S T U} → Overload F (R ⇒ S) → ((R ⇒ S) <: (T ⇒ U)) → F <: (T ⇒ U)
+ov-<: : ∀ {F R S T U} → FunType F → Overloads F (R ⇒ S) → ((R ⇒ S) <: (T ⇒ U)) → F <: (T ⇒ U)
-ov-<: here p = p
+ov-<: F never p = <:-trans (<:-trans (function-top {!!}) <:-function-never) p
-ov-<: (left o) p = <:-trans <:-∩-left (ov-<: o p)
+ov-<: F here p = p
-ov-<: (right o) p = <:-trans <:-∩-right (ov-<: o p)
+ov-<: (F ∩ G) (left o) p = <:-trans <:-∩-left (ov-<: F o p)
+ov-<: (F ∩ G) (right o) p = <:-trans <:-∩-right (ov-<: G o p)
 
-⊆ᵒ-left : ∀ {F G} → F ⊆ᵒ (F ∩ G)
+⊂:-overloads-left : ∀ {F G} → Overloads F ⊂: Overloads (F ∩ G)
-⊆ᵒ-left = left
+⊂:-overloads-left = {!!}
 
-⊆ᵒ-right : ∀ {F G} → G ⊆ᵒ (F ∩ G)
+⊂:-overloads-right : ∀ {F G} → Overloads G ⊂: Overloads (F ∩ G)
-⊆ᵒ-right = right
+⊂:-overloads-right = {!!}
 
-⋒-cl-∩ : ∀ {F} → (F ⋒ F) ⊂:ᵒ F → ∀ {R S T U} → Overload F (R ⇒ S) → Overload F (T ⇒ U) → F <:ᵒ ((R ∩ T) ⇒ (S ∩ U))
+⊂:-overloads-⋒ : ∀ {F G} → FunType F → FunType G → ∩-Lift (Overloads F) (Overloads G) ⊂: Overloads (F ⋒ G)
-⋒-cl-∩ = {!!}
+⊂:-overloads-⋒ F G = {!!}
 
-⋓-cl-∪ : ∀ {F} → (F ⋓ F) ⊂:ᵒ F → ∀ {R S T U} → Overload F (R ⇒ S) → Overload F (T ⇒ U) → F <:ᵒ ((R ∪ T) ⇒ (S ∪ U))
+⊂:-⋒-overloads : ∀ {F G} → FunType F → FunType G → Overloads (F ⋒ G) ⊂: ∩-Lift (Overloads F) (Overloads G)
-⋓-cl-∪ = {!!}
+⊂:-⋒-overloads F G = {!!}
 
--- The overloads of (F ⋓ G) are unions of overloads from F and G
+∪-saturate-overloads : ∀ {F} → FunType F → Overloads (∪-saturate F) ⊂: ∪-Saturate (Overloads F)
-data ⋓-Overload F G : Type → Set where
+∪-saturate-overloads F = {!!}
 
-  defn : ∀ {R S T U} →
+overloads-∪-saturate : ∀ {F} → FunType F → ∪-Saturate (Overloads F) ⊂: Overloads (∪-saturate F)
+overloads-∪-saturate F = {!!}
 
-    Overload F (R ⇒ S) →
+∪-saturated : ∀ {F} → FunType F → ∪-Lift (Overloads (∪-saturate F)) (Overloads (∪-saturate F)) ⊂: Overloads (∪-saturate F)
-    Overload G (T ⇒ U) →
+∪-saturated F = {!!}
-    ---------------------------
-    ⋓-Overload F G ((R ∪ T) ⇒ (S ∪ U))
 
-⋓-∪-overload : ∀ F G {S T} → Overload (F ⋓ G) (S ⇒ T) → ⋓-Overload F G (S ⇒ T)
+∩-saturate-overloads : ∀ {F} → FunType F → Overloads (∩-saturate F) ⊂: ∩-Saturate (Overloads F)
-⋓-∪-overload = {!!}
+∩-saturate-overloads F = {!!}
 
--- Properties of ⊂:ᵒ 
+overloads-∩-saturate : ∀ {F} → FunType F → ∩-Saturate (Overloads F) ⊂: Overloads (∩-saturate F)
-⊂:ᵒ-refl : ∀ {F} → (F ⊂:ᵒ F)
+overloads-∩-saturate F = ⊂:-∩-saturate-indn (inj F) (step F) where
-⊂:ᵒ-refl o = defn o (λ t z → z) (λ t z → z)
-
-⊂:ᵒ-trans : ∀ {F G H} → (F ⊂:ᵒ G) → (G ⊂:ᵒ H) → (F ⊂:ᵒ H)  
-⊂:ᵒ-trans = {!!}
-
-⊂:ᵒ-left : ∀ {F G H} → (F ⊂:ᵒ G) → (F ⊂:ᵒ (G ∩ H))  
-⊂:ᵒ-left = {!!}
-
-⊂:ᵒ-right : ∀ {F G H} → (F ⊂:ᵒ H) → (F ⊂:ᵒ (G ∩ H))  
-⊂:ᵒ-right = {!!}
-
-⊂:ᵒ-lub : ∀ {F G H} → (F ⊂:ᵒ H) → (G ⊂:ᵒ H) → ((F ∩ G) ⊂:ᵒ H)  
-⊂:ᵒ-lub = {!!}
-
-⊂:ᵒ-⋓-symm : ∀ {F G} → ((F ⋓ G) ⊂:ᵒ (G ⋓ F))
-⊂:ᵒ-⋓-symm = {!!}
-
-⊂:ᵒ-⋓-assocl : ∀ {F G H} → (F ⋓ (G ⋓ H)) ⊂:ᵒ ((F ⋓ G) ⋓ H)
-⊂:ᵒ-⋓-assocl = {!!}
-
-⊂:ᵒ-⋓-assocr : ∀ {F G H} → ((F ⋓ G) ⋓ H) ⊂:ᵒ (F ⋓ (G ⋓ H))
-⊂:ᵒ-⋓-assocr = {!!}
-
-⊂:ᵒ-⋓-redist : ∀ {E F G H} → ((E ⋓ F) ⋓ (G ⋓ H)) ⊂:ᵒ ((E ⋓ G) ⋓ (F ⋓ H))
-⊂:ᵒ-⋓-redist = {!!}
-
-⊂:ᵒ-⋓-dist-∩ : ∀ F G H → (F ⋓ (G ∩ H)) ⊂:ᵒ ((F ⋓ G) ∩ (F ⋓ H))
-⊂:ᵒ-⋓-dist-∩ = {!!}
-
-⊂:ᵒ-⋓-dist-⋒ : ∀ {F G H} → (F ⋓ (G ⋒ H)) ⊂:ᵒ ((F ⋓ G) ⋒ (F ⋓ H))
-⊂:ᵒ-⋓-dist-⋒ = {!!}
-
-⊂:ᵒ-⋓ : ∀ {E F G H} → (E ⊂:ᵒ F) → (G ⊂:ᵒ H) → ((E ⋓ G) ⊂:ᵒ (F ⋓ H))
-⊂:ᵒ-⋓ = {!!}
-
-⊂:ᵒ-⋒ : ∀ {E F G H} → (E ⊂:ᵒ F) → (G ⊂:ᵒ H) → ((E ⋒ G) ⊂:ᵒ (F ⋒ H))
-⊂:ᵒ-⋒ = {!!}
-
--- Every function can be ∪-saturated!
-∩ᵘ-∪-saturated : ∀ {F G} → (F ⋓ F) ⊂:ᵒ F → (G ⋓ G) ⊂:ᵒ G → ((F ∩ᵘ G) ⋓ (F ∩ᵘ G)) ⊂:ᵒ (F ∩ᵘ G)
-∩ᵘ-∪-saturated {F} {G} Fˢ Gˢ = ⊂:ᵒ-trans
-  (⊂:ᵒ-⋓-dist-∩ (F ∩ᵘ G) (F ∩ G) (F ⋓ G))
-  (⊂:ᵒ-lub (⊂:ᵒ-lub (⊂:ᵒ-lub
-    (⊂:ᵒ-trans (⊂:ᵒ-⋓-dist-∩ F F G) (⊂:ᵒ-lub (⊂:ᵒ-trans Fˢ (⊂:ᵒ-left (⊂:ᵒ-left ⊂:ᵒ-refl))) (⊂:ᵒ-right ⊂:ᵒ-refl)))
-    (⊂:ᵒ-trans (⊂:ᵒ-⋓-dist-∩ G F G) (⊂:ᵒ-lub (⊂:ᵒ-right (⊂:ᵒ-⋓-symm {G})) (⊂:ᵒ-trans Gˢ (⊂:ᵒ-left (⊂:ᵒ-right ⊂:ᵒ-refl))))))
-    (⊂:ᵒ-trans (⊂:ᵒ-⋓-dist-∩ (F ⋓ G) F G) (⊂:ᵒ-lub (⊂:ᵒ-right (⊂:ᵒ-trans (⊂:ᵒ-⋓-symm {F ⋓ G}) (⊂:ᵒ-trans (⊂:ᵒ-⋓-assocl {F}) (⊂:ᵒ-⋓ Fˢ ⊂:ᵒ-refl)))) (⊂:ᵒ-trans (⊂:ᵒ-⋓-assocr {F}) (⊂:ᵒ-right (⊂:ᵒ-⋓ (⊂:ᵒ-refl {F}) Gˢ))))))
-    (⊂:ᵒ-lub (⊂:ᵒ-lub
-      (⊂:ᵒ-trans (⊂:ᵒ-⋓-assocl {F}) (⊂:ᵒ-right (⊂:ᵒ-⋓ Fˢ ⊂:ᵒ-refl)))
-      (⊂:ᵒ-trans (⊂:ᵒ-⋓-symm {G}) (⊂:ᵒ-trans (⊂:ᵒ-⋓-assocr {F}) (⊂:ᵒ-right (⊂:ᵒ-⋓ (⊂:ᵒ-refl {F}) Gˢ)))))
-      (⊂:ᵒ-trans (⊂:ᵒ-⋓-redist {F}) (⊂:ᵒ-right (⊂:ᵒ-⋓ Fˢ Gˢ)))))
-
-⊆ᵒ-∪-sat : ∀ {F} → F ⊆ᵒ ∪-saturate F
-⊆ᵒ-∪-sat here = here
-⊆ᵒ-∪-sat (left o) = left (left (⊆ᵒ-∪-sat o))
-⊆ᵒ-∪-sat (right o) = left (right (⊆ᵒ-∪-sat o))
-
-∪-∪-saturated : ∀ {F} → (FunType F) → (∪-saturate F ⋓ ∪-saturate F) ⊂:ᵒ ∪-saturate F
-∪-∪-saturated function here = <:ᵒ-refl
-∪-∪-saturated (Sⁱ ⇒ Tⁿ) here = defn here (<:-trans (∪ⁿ-<:-∪ (normalⁱ Sⁱ) (normalⁱ Sⁱ)) (<:-∪-lub <:-refl <:-refl)) (<:-trans (<:-trans <:-∪-left (∪-<:-∪ⁿ Tⁿ Tⁿ)) <:-tgtⁿ)
-∪-∪-saturated (Fᶠ ∩ Gᶠ) o = ∩ᵘ-∪-saturated (∪-∪-saturated Fᶠ) (∪-∪-saturated Gᶠ) o
-
--- ∩-saturate is ⋓-closed
-∪-saturated : ∀ {F} → (FunType F) → (saturate F ⋓ saturate F) ⊂:ᵒ saturate F
-∪-saturated F = ∪-∪-saturated (normal-∩-saturate F)
-
--- ∩-saturate is ⋒-closed
-ov-⋒-∩ : ∀ {F G R S T U} → FunType F → FunType G → Overload F (R ⇒ S) → Overload G (T ⇒ U) → (F ⋒ G) <:ᵒ ((R ∩ T) ⇒ (S ∩ U))
-ov-⋒-∩ function function here here = defn here (∩-<:-∩ⁿ never never) (<:-∩-glb <:-refl <:-refl)
-ov-⋒-∩ function (T ⇒ U) here here = defn here (∩-<:-∩ⁿ never (normalⁱ T)) {!<:-tgtⁿ (∩ⁿ-<:-∩ unknown U)!}
-ov-⋒-∩ function (G ∩ H) here (left o) = {!!}
-ov-⋒-∩ function (G ∩ H) here (right o) = {!!}
-ov-⋒-∩ (R ⇒ S) function here here = defn here (∩-<:-∩ⁿ {!!} {!!}) {!!}
-ov-⋒-∩ (R ⇒ S) (T ⇒ U) here here = defn here (∩-<:-∩ⁿ {!!} {!!}) {!!}
-ov-⋒-∩ (R ⇒ S) (G ∩ H) here (left o) = {!!}
-ov-⋒-∩ (R ⇒ S) (G ∩ H) here (right o) = {!!}
-ov-⋒-∩ (E ∩ F) function n o = {!!}
-ov-⋒-∩ (E ∩ F) (T ⇒ U) n o = {!!}
-ov-⋒-∩ (E ∩ F) (G ∩ H) n o = {!!}
-
-∩-∩-saturated : ∀ {F} → (FunType F) → (∩-saturate F ⋒ ∩-saturate F) ⊂:ᵒ ∩-saturate F
-∩-∩-saturated F = {!!}
-
--- An inductive presentation of the ⋒-overloads of a type
-data ⋒-Overload F G : Type → Set where
-
-  defn : ∀ {R S T U} →
-
-    Overload F (R ⇒ S) →
-    Overload G (T ⇒ U) →
-    ---------------------------
-    ⋒-Overload F G ((R ∩ T) ⇒ (S ∩ U))
-
-data ⋒-Overload-<: F G : Type → Set where
- 
-  defn : ∀ {R S T U} →
-
-    ⋒-Overload F G (R ⇒ S) →
-    T <: R →
-    S <: U →
-    ---------------------
-    ⋒-Overload-<: F G (T ⇒ U)
-
-⋒-overload-<: : ∀ {F G S T} → FunType F → FunType G → Overload (F ⋒ G) (S ⇒ T) → ⋒-Overload-<: F G (S ⇒ T)
-⋒-overload-<: function function here = defn (defn here here) <:-never <:-unknown
-⋒-overload-<: function (T ⇒ U) here = defn (defn here here) (∩ⁿ-<:-∩ never (normalⁱ T)) (<:-trans (∩-<:-∩ⁿ unknown U) <:-tgtⁿ)
-⋒-overload-<: function (G ∩ H) (left o) with ⋒-overload-<: function G o
-⋒-overload-<: function (G ∩ H) (left o) | defn (defn o₁ o₂) o₃ o₄ = defn (defn o₁ (left o₂)) o₃ o₄
-⋒-overload-<: function (G ∩ H) (right o) with ⋒-overload-<: function H o
-⋒-overload-<: function (G ∩ H) (right o) | defn (defn o₁ o₂) o₃ o₄ = defn (defn o₁ (right o₂)) o₃ o₄
-⋒-overload-<: (R ⇒ S) function here = defn (defn here here) (∩ⁿ-<:-∩ (normalⁱ R) never) (<:-trans (∩-<:-∩ⁿ S unknown) <:-tgtⁿ)
-⋒-overload-<: (R ⇒ S) (T ⇒ U) here = defn (defn here here) (∩ⁿ-<:-∩ (normalⁱ R) (normalⁱ T)) (<:-trans (∩-<:-∩ⁿ S U) <:-tgtⁿ)
-⋒-overload-<: (R ⇒ S) (G ∩ H) (left o) with ⋒-overload-<: (R ⇒ S) G o
-⋒-overload-<: (R ⇒ S) (G ∩ H) (left o) | defn (defn o₁ o₂) o₃ o₄ = defn (defn o₁ (left o₂)) o₃ o₄
-⋒-overload-<: (R ⇒ S) (G ∩ H) (right o) with ⋒-overload-<: (R ⇒ S) H o
-⋒-overload-<: (R ⇒ S) (G ∩ H) (right o) | defn (defn o₁ o₂) o₃ o₄ = defn (defn o₁ (right o₂)) o₃ o₄
-⋒-overload-<: (E ∩ F) G (left o) with ⋒-overload-<: E G o
-⋒-overload-<: (E ∩ F) G (left o) | defn (defn o₁ o₂) o₃ o₄ = defn (defn (left o₁) o₂) o₃ o₄
-⋒-overload-<: (E ∩ F) G (right o) with ⋒-overload-<: F G o
-⋒-overload-<: (E ∩ F) G (right o) | defn (defn o₁ o₂) o₃ o₄ = defn (defn (right o₁) o₂) o₃ o₄
-
--- An inductive presentation of the ⋓-closure of a type
-data ⋓-Closure F : Type → Set where
-
-  ov : ∀ {S T} →
   
-    Overload F (S ⇒ T) →
+  inj :  ∀ {F} → FunType F → Overloads F ⊂: Overloads (∩-saturate F)
-    -------------------
+  inj = {!!}
-    ⋓-Closure F (S ⇒ T)
 
-  union : ∀ {R S T U} →
+  step : ∀ {F} → FunType F → ∩-Lift (Overloads (∩-saturate F)) (Overloads (∩-saturate F)) ⊂: Overloads (∩-saturate F)
+  step function (intersect here here) = defn here <:-∩-left (<:-∩-glb <:-refl <:-refl)
+  step (S ⇒ T) (intersect here here) = defn here <:-∩-left (<:-∩-glb <:-refl <:-refl)
+  step (F ∩ G) (intersect (left (left p)) (left (left q))) = step F (intersect p q) >>= ⊂:-overloads-left >>= ⊂:-overloads-left
+  step (F ∩ G) (intersect (left (left p)) (left (right q))) = ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) (intersect p q) >>= ⊂:-overloads-right
+  step (F ∩ G) (intersect (left (right p)) (left (left q))) = ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) (intersect q p) >>= ⊂:-overloads-right >>=ˡ <:-∩-symm >>=ʳ <:-∩-symm
+  step (F ∩ G) (intersect (left (right p)) (left (right q))) = step G (intersect p q) >>= ⊂:-overloads-right >>= ⊂:-overloads-left
+  step (F ∩ G) (intersect (right p) q) with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) p
+  step (F ∩ G) (intersect (right p) (left (left q))) | defn (intersect p₁ p₂) p₃ p₄ =
+    (step F (intersect p₁ q) [∩] just p₂) >>=
+    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
+    ⊂:-overloads-right >>=ˡ
+    <:-trans (<:-intersect p₃ <:-refl) (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-trans <:-∩-left <:-∩-right)) >>=ʳ
+    <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-refl) (<:-trans <:-∩-left <:-∩-right)) (<:-intersect p₄ <:-refl)
+  step (F ∩ G) (intersect (right p) (left (right q))) | defn (intersect p₁ p₂) p₃ p₄ =
+    (just p₁ [∩] step G (intersect p₂ q)) >>=
+    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
+    ⊂:-overloads-right >>=ˡ
+    <:-trans (<:-intersect p₃ <:-refl) <:-∩-assocr >>=ʳ
+    <:-trans <:-∩-assocl (<:-intersect p₄ <:-refl)
+  step (F ∩ G) (intersect (right p) (right q)) | defn (intersect p₁ p₂) p₃ p₄ with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) q
+  step (F ∩ G) (intersect (right p) (right q)) | defn (intersect p₁ p₂) p₃ p₄ | defn (intersect q₁ q₂) q₃ q₄ =
+    (step F (intersect p₁ q₁) [∩] step G (intersect p₂ q₂)) >>=
+    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
+    ⊂:-overloads-right >>=ˡ
+    <:-trans (<:-intersect p₃ q₃) (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) >>=ʳ
+    <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) (<:-intersect p₄ q₄)
+  step (F ∩ G) (intersect (right p) (left never)) | defn (intersect p₁ p₂) p₃ p₄ = defn never <:-∩-right <:-never
+  step (F ∩ G) (intersect (right p) never) | defn (intersect p₁ p₂) p₃ p₄ = defn never <:-∩-right <:-never
+  step (F ∩ G) (intersect p (right q)) with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) q
+  step (F ∩ G) (intersect (left (left p)) (right q)) | defn (intersect q₁ q₂) q₃ q₄ =
+    (step F (intersect p q₁) [∩] just q₂) >>=
+    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
+    ⊂:-overloads-right >>=ˡ
+    <:-trans (<:-intersect <:-refl q₃) <:-∩-assocl >>=ʳ
+    <:-trans <:-∩-assocr (<:-intersect <:-refl q₄)
+  step (F ∩ G) (intersect (left (right p)) (right q)) | defn (intersect q₁ q₂) q₃ q₄ =
+    (just q₁ [∩] step G (intersect p q₂) ) >>=
+    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
+    ⊂:-overloads-right >>=ˡ
+    <:-trans (<:-intersect <:-refl q₃) (<:-∩-glb (<:-trans <:-∩-right <:-∩-left) (<:-∩-glb <:-∩-left (<:-trans <:-∩-right <:-∩-right))) >>=ʳ
+    <:-∩-glb (<:-trans <:-∩-right <:-∩-left) (<:-trans (<:-∩-glb <:-∩-left (<:-trans <:-∩-right <:-∩-right)) q₄)
+  step (F ∩ G) (intersect (right p) (right q)) | defn (intersect q₁ q₂) q₃ q₄ with ⊂:-⋒-overloads (normal-∩-saturate F) (normal-∩-saturate G) p
+  step (F ∩ G) (intersect (right p) (right q)) | defn (intersect q₁ q₂) q₃ q₄ | defn (intersect p₁ p₂) p₃ p₄ =
+    (step F (intersect p₁ q₁) [∩] step G (intersect p₂ q₂)) >>=
+    ⊂:-overloads-⋒ (normal-∩-saturate F) (normal-∩-saturate G) >>=
+    ⊂:-overloads-right >>=ˡ
+    <:-trans (<:-intersect p₃ q₃) (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) >>=ʳ
+    <:-trans (<:-∩-glb (<:-intersect <:-∩-left <:-∩-left) (<:-intersect <:-∩-right <:-∩-right)) (<:-intersect p₄ q₄)
+  step (F ∩ G) (intersect never (right q)) | defn (intersect q₁ q₂) q₃ q₄ = defn never <:-∩-left <:-never
+  step (F ∩ G) (intersect (left never) (right q)) | defn (intersect q₁ q₂) q₃ q₄ = defn never <:-∩-left <:-never
+  step (F ∩ G) (intersect (left never) q) = defn never <:-∩-left <:-never
+  step (F ∩ G) (intersect p (left never)) = defn never <:-∩-right <:-never
+  step F (intersect never q) = defn never <:-∩-left <:-never
+  step F (intersect p never) = defn never <:-∩-right <:-never
 
-    ⋓-Closure F (R ⇒ S) →
+saturate-overloads : ∀ {F} → FunType F → Overloads (saturate F) ⊂: ∪-Saturate (∩-Saturate (Overloads F))
-    ⋓-Closure F (T ⇒ U) →
+saturate-overloads F o = ∪-saturate-overloads (normal-∩-saturate F) o >>= (⊂:-∪-saturate (∩-saturate-overloads F))
-    -------------------------------
-    ⋓-Closure F ((R ∪ T) ⇒ (S ∪ U))
 
-data ⋓-Closure-<: F : Type → Set where
+overloads-saturate : ∀ {F} → FunType F → ∪-Saturate (∩-Saturate (Overloads F)) ⊂: Overloads (saturate F)
- 
+overloads-saturate F o = ⊂:-∪-saturate (overloads-∩-saturate F) o >>= overloads-∪-saturate (normal-∩-saturate F)
-  defn : ∀ {R S T U} →
 
-    ⋓-Closure F (R ⇒ S) →
+-- Saturated F whenever
-    T <: R →
+-- * if F has overloads (R ⇒ S) and (T ⇒ U) then F has an overload which is a subtype of ((R ∩ T) ⇒ (S ∩ U))
-    S <: U →
+-- * ditto union
-    ---------------------
+data Saturated (F : Type) : Set where
-    ⋓-Closure-<: F (T ⇒ U)
 
-⋓-closure-resp-⊆ᵒ : ∀ {F G S T} → (F ⊆ᵒ G) → ⋓-Closure F (S ⇒ T) → ⋓-Closure G (S ⇒ T)
+  defn : 
-⋓-closure-resp-⊆ᵒ p (ov o) = ov (p o)
-⋓-closure-resp-⊆ᵒ p (union c d) = union (⋓-closure-resp-⊆ᵒ p c) (⋓-closure-resp-⊆ᵒ p d)
 
-∪-saturate-overload-impl-⋓-closure : ∀ {F S T} → FunType F → Overload (∪-saturate F) (S ⇒ T) → ⋓-Closure F (S ⇒ T)
+    (∀ {R S T U} → Overloads F (R ⇒ S) → Overloads F (T ⇒ U) → F <:ᵒ ((R ∩ T) ⇒ (S ∩ U))) →
-∪-saturate-overload-impl-⋓-closure function here = ov here
+    (∀ {R S T U} → Overloads F (R ⇒ S) → Overloads F (T ⇒ U) → F <:ᵒ ((R ∪ T) ⇒ (S ∪ U))) →
-∪-saturate-overload-impl-⋓-closure (S ⇒ T) here = ov here
+    -----------
-∪-saturate-overload-impl-⋓-closure (Fᶠ ∩ Gᶠ) (left (left o)) = ⋓-closure-resp-⊆ᵒ ⊆ᵒ-left (∪-saturate-overload-impl-⋓-closure Fᶠ o)
+    Saturated F
-∪-saturate-overload-impl-⋓-closure (Fᶠ ∩ Gᶠ) (left (right o)) = ⋓-closure-resp-⊆ᵒ ⊆ᵒ-right (∪-saturate-overload-impl-⋓-closure Gᶠ o)
-∪-saturate-overload-impl-⋓-closure {F ∩ G} (Fᶠ ∩ Gᶠ) (right o) with ⋓-∪-overload (∪-saturate F) (∪-saturate G) o
-∪-saturate-overload-impl-⋓-closure (Fᶠ ∩ Gᶠ) (right o) | defn p q = union (⋓-closure-resp-⊆ᵒ ⊆ᵒ-left (∪-saturate-overload-impl-⋓-closure Fᶠ p)) (⋓-closure-resp-⊆ᵒ ⊆ᵒ-right (∪-saturate-overload-impl-⋓-closure Gᶠ q))
 
-⋓-closure-impl-∪-saturate-<:ᵒ : ∀ {F S T} → (FunType F) → ⋓-Closure F (S ⇒ T) → (∪-saturate F) <:ᵒ (S ⇒ T)
+-- saturated F is saturated!
-⋓-closure-impl-∪-saturate-<:ᵒ Fᶠ (ov o) = <:ᵒ-ov (⊆ᵒ-∪-sat o)
+saturated : ∀ {F} → FunType F → Saturated (saturate F)
-⋓-closure-impl-∪-saturate-<:ᵒ Fᶠ (union c d) with ⋓-closure-impl-∪-saturate-<:ᵒ Fᶠ c | ⋓-closure-impl-∪-saturate-<:ᵒ Fᶠ d
+saturated F = defn
-⋓-closure-impl-∪-saturate-<:ᵒ Fᶠ (union c d) | defn o o₁ o₂ | defn p p₁ p₂ = <:ᵒ-trans-<: (⋓-cl-∪ (∪-∪-saturated Fᶠ) o p) (<:-union o₁ p₁) (<:-union o₂ p₂)
+  (λ n o → (saturate-overloads F n [∩] saturate-overloads F o) >>= ∪-saturate-resp-∩-saturation ⊂:-∩-lift-saturate >>= overloads-saturate F)
-
+  (λ n o → ∪-saturated (normal-∩-saturate F) (union n o))
-⋓-closure-<:ᵒ : ∀ {F S T} → F <:ᵒ (S ⇒ T) → ⋓-Closure-<: F (S ⇒ T)
-⋓-closure-<:ᵒ (defn o p q) = defn (ov o) p q
-
-⋓-closure-<:-∩ : ∀ {F R S T U} → (FunType F) → (F ⋒ F) ⊂:ᵒ F → ⋓-Closure F (R ⇒ S) → ⋓-Closure F (T ⇒ U) → ⋓-Closure-<: F ((R ∩ T) ⇒ (S ∩ U))
-⋓-closure-<:-∩ Fᶠ p (ov n) (ov o) with ov-⋒-∩ Fᶠ Fᶠ n o
-⋓-closure-<:-∩ Fᶠ p (ov n) (ov o) | defn q q₁ q₂ = ⋓-closure-<:ᵒ (<:ᵒ-trans-<: (p q) q₁ q₂)
-⋓-closure-<:-∩ Fᶠ p c (union d d₁) with ⋓-closure-<:-∩ Fᶠ p c d | ⋓-closure-<:-∩ Fᶠ p c d₁ 
-⋓-closure-<:-∩ Fᶠ p c (union d d₁) | defn e e₁ e₂ | defn f f₁ f₂ = defn (union e f) (<:-trans <:-∩-distl-∪ (<:-union e₁ f₁)) (<:-trans (<:-union e₂ f₂) ∩-distl-∪-<:)
-⋓-closure-<:-∩ Fᶠ p (union c c₁) d with ⋓-closure-<:-∩ Fᶠ p c d | ⋓-closure-<:-∩ Fᶠ p c₁ d
-⋓-closure-<:-∩ Fᶠ p (union c c₁) d | defn e e₁ e₂ | defn f f₁ f₂ = defn (union e f) (<:-trans <:-∩-distr-∪ (<:-union e₁ f₁)) (<:-trans (<:-union e₂ f₂) ∩-distr-∪-<:)
-
--- ∪-saturate preserves ⋒-closure
-∪-saturate-⋒-closed : ∀ {F} → (FunType F) → (F ⋒ F) ⊂:ᵒ F → (∪-saturate F ⋒ ∪-saturate F) ⊂:ᵒ ∪-saturate F
-∪-saturate-⋒-closed Fᶠ p o with ⋒-overload-<: (normal-∪-saturate Fᶠ) (normal-∪-saturate Fᶠ) o
-∪-saturate-⋒-closed Fᶠ p o | defn (defn o₁ o₂) o₃ o₄ with ∪-saturate-overload-impl-⋓-closure Fᶠ o₁ | ∪-saturate-overload-impl-⋓-closure Fᶠ o₂ 
-∪-saturate-⋒-closed Fᶠ p o | defn (defn o₁ o₂) o₃ o₄ | c₁ | c₂ with ⋓-closure-<:-∩ Fᶠ p c₁ c₂
-∪-saturate-⋒-closed Fᶠ p o | defn (defn o₁ o₂) o₃ o₄ | c₁ | c₂ | defn d q r = <:ᵒ-trans-<: (⋓-closure-impl-∪-saturate-<:ᵒ Fᶠ d) (<:-trans o₃ q) (<:-trans r o₄)
-
--- so saturate is ⋒-closed
-saturated-is-⋒-closed : ∀ {F} → (FunType F) → (saturate F ⋒ saturate F) ⊂:ᵒ saturate F
-saturated-is-⋒-closed F = ∪-saturate-⋒-closed (normal-∩-saturate F) (∩-∩-saturated F)
-
--- Every function type can be saturated!
-saturated : ∀ {F} → (FunType F) → Saturated (saturate F)
-saturated F = ⋒-⋓-cl-impl-sat (saturated-is-⋒-closed F) (∪-saturated F)
 
 -- Subtyping is decidable on saturated normalized types
 
 dec-<:-overloads : ∀ {F S T} → FunType F → FunType (S ⇒ T) → Saturated F →
-  (∀ {S′ T′} → (Overload F (S′ ⇒ T′)) → Either (S ≮: S′) (S <: S′)) →
+  (∀ {S′ T′} → (Overloads F (S′ ⇒ T′)) → Either (S ≮: S′) (S <: S′)) →
-  (∀ {S′ T′} → (Overload F (S′ ⇒ T′)) → Either (T′ ≮: T) (T′ <: T)) →
+  (∀ {S′ T′} → (Overloads F (S′ ⇒ T′)) → Either (T′ ≮: T) (T′ <: T)) →
   Either (F ≮: (S ⇒ T)) (F <: (S ⇒ T))
 dec-<:-overloads {F} {S} {T} Fᶠ function _ _ _ = Right (function-top Fᶠ)
-dec-<:-overloads {F} {S} {T} Fᶠ (Sⁱ ⇒ Tⁿ) (defn sat-∩ sat-∪) dec-src dec-tgt = result (top Fᶠ (λ o → o)) (bot Fᶠ (λ o → o)) where
+dec-<:-overloads {F} {S} {T} Fᶠ (Sⁱ ⇒ Tⁿ) (defn sat-∩ sat-∪) dec-src dec-tgt = result (top Fᶠ (λ o → o)) where
 
   data Top G : Set where
 
     defn : ∀ Sᵗ Tᵗ →
 
-      Overload F (Sᵗ ⇒ Tᵗ) →
+      Overloads F (Sᵗ ⇒ Tᵗ) →
-      (∀ {S′ T′} → Overload G (S′ ⇒ T′) → (S′ <: Sᵗ)) →
+      (∀ {S′ T′} → Overloads G (S′ ⇒ T′) → (S′ <: Sᵗ)) →
       -------------
       Top G
 
-  data Bot G : Set where
-
-    defn : ∀ Sᵇ Tᵇ →
-
-      Overload F (Sᵇ ⇒ Tᵇ) →
-      (∀ {S′ T′} → Overload G (S′ ⇒ T′) → (Tᵇ <: T′)) →
-      -------------
-      Bot G
-
   top : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → Top G
-  top {S′ ⇒ T′} _ G⊆F = defn S′ T′ (G⊆F here) (λ { here → <:-refl })
+  top {S′ ⇒ T′} _ G⊆F = defn S′ T′ (G⊆F here) (λ { here → <:-refl ; never → <:-never })
   top (Gᶠ ∩ Hᶠ) G⊆F with top Gᶠ (G⊆F ∘ left) | top Hᶠ (G⊆F ∘ right)
   top (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵗ Sᵗ p p₁ | defn Tᵗ Uᵗ q q₁ with sat-∪ p q
   top (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵗ Sᵗ p p₁ | defn Tᵗ Uᵗ q q₁ | defn n r r₁ = defn _ _ n
-    (λ { (left o) → <:-trans (<:-trans (p₁ o) <:-∪-left) r ; (right o) → <:-trans (<:-trans (q₁ o) <:-∪-right) r })
+    (λ { (left o) → <:-trans (<:-trans (p₁ o) <:-∪-left) r ; (right o) → <:-trans (<:-trans (q₁ o) <:-∪-right) r ; never → <:-never })
 
-  bot : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → Bot G
+  result : Top F → Either (F ≮: (S ⇒ T)) (F <: (S ⇒ T))
-  bot {S′ ⇒ T′} _ G⊆F = defn S′ T′ (G⊆F here) (λ { here → <:-refl })
+  result (defn Sᵗ Tᵗ oᵗ srcᵗ) with dec-src oᵗ
-  bot (Gᶠ ∩ Hᶠ) G⊆F with bot Gᶠ (G⊆F ∘ left) | bot Hᶠ (G⊆F ∘ right)
+  result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Left (witness s Ss ¬Sᵗs) = Left (witness (function-err s) (ov-language Fᶠ (λ o → function-err (<:-impl-⊇ (srcᵗ o) s ¬Sᵗs))) (function-err Ss))
-  bot (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵇ Sᵇ p p₁ | defn Tᵇ Uᵇ q q₁ with sat-∩ p q
+  result (defn Sᵗ Tᵗ oᵗ srcᵗ) | Right S<:Sᵗ = result₀ (largest Fᶠ (λ o → o)) where
-  bot (Gᶠ ∩ Hᶠ) G⊆F | defn Rᵇ Sᵇ p p₁ | defn Tᵇ Uᵇ q q₁ | defn n r r₁ = defn _ _ n
-    (λ { (left o) → <:-trans (<:-trans r₁ <:-∩-left) (p₁ o) ; (right o) → <:-trans (<:-trans r₁ <:-∩-right) (q₁ o) })
-
-  result : Top F → Bot F → Either (F ≮: (S ⇒ T)) (F <: (S ⇒ T))
-  result (defn Sᵗ Tᵗ oᵗ srcᵗ) (defn Sᵇ Tᵇ oᵇ tgtᵇ) with dec-src oᵗ | dec-tgt oᵇ
-  result (defn Sᵗ Tᵗ oᵗ srcᵗ) (defn Sᵇ Tᵇ oᵇ tgtᵇ) | Left (witness s Ss ¬Sᵗs) | _ = Left (witness (function-err s) (ov-language Fᶠ (λ o → function-err (<:-impl-⊇ (srcᵗ o) s ¬Sᵗs))) (function-err Ss))
-  result (defn Sᵗ Tᵗ oᵗ srcᵗ) (defn Sᵇ Tᵇ oᵇ tgtᵇ) | _ | Left (witness t Tᵇt ¬Tt) = Left (witness (function-ok (inhabitant Sⁱ) t) (ov-language Fᶠ (λ o → function-ok₂ (tgtᵇ o t Tᵇt))) (function-ok (inhabited Sⁱ) ¬Tt))
-  result (defn Sᵗ Tᵗ oᵗ srcᵗ) (defn Sᵇ Tᵇ oᵇ tgtᵇ) | Right S<:Sᵗ | Right Tᵇ<:T = result₀ (largest Fᶠ (λ o → o)) where
 
     data LargestSrc (G : Type) : Set where
 
       defn : ∀ S₀ T₀ →
 
-        Overload F (S₀ ⇒ T₀) →
+        Overloads F (S₀ ⇒ T₀) →
         T₀ <: T →
-        (∀ {S′ T′} → Overload G (S′ ⇒ T′) → T′ <: T → (S′ <: S₀)) →
+        (∀ {S′ T′} → Overloads G (S′ ⇒ T′) → T′ <: T → (S′ <: S₀)) →
         -----------------------
         LargestSrc G
 
     largest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → LargestSrc G
     largest {S′ ⇒ T′} _ G⊆F with dec-tgt (G⊆F here)
-    largest {S′ ⇒ T′} _ G⊆F | Left T′≮:T = defn Sᵇ Tᵇ oᵇ Tᵇ<:T (λ { here T′<:T → CONTRADICTION (<:-impl-¬≮: T′<:T T′≮:T) })
+    largest {S′ ⇒ T′} _ G⊆F | Left T′≮:T = defn never never never <:-never (λ { here T′<:T → CONTRADICTION (<:-impl-¬≮: T′<:T T′≮:T) ; never _ → <:-never })
-    largest {S′ ⇒ T′} _ G⊆F | Right T′<:T = defn S′ T′ (G⊆F here) T′<:T (λ { here _ → <:-refl })
+    largest {S′ ⇒ T′} _ G⊆F | Right T′<:T = defn S′ T′ (G⊆F here) T′<:T (λ { here _ → <:-refl  ; never _ → <:-never })
     largest (Gᶠ ∩ Hᶠ) GH⊆F with largest Gᶠ (GH⊆F ∘ left) | largest Hᶠ (GH⊆F ∘ right)
     largest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ T₁<:T src₁ | defn S₂ T₂ o₂ T₂<:T src₂ with sat-∪ o₁ o₂
     largest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ T₁<:T src₁ | defn S₂ T₂ o₂ T₂<:T src₂ | defn o src tgt = defn _ _ o (<:-trans tgt (<:-∪-lub T₁<:T T₂<:T))
-      (λ { (left o) T′<:T → <:-trans (src₁ o T′<:T) (<:-trans <:-∪-left src) ; (right o) T′<:T → <:-trans (src₂ o T′<:T) (<:-trans <:-∪-right src) })
+      (λ { (left o) T′<:T → <:-trans (src₁ o T′<:T) (<:-trans <:-∪-left src)
+         ; (right o) T′<:T → <:-trans (src₂ o T′<:T) (<:-trans <:-∪-right src)
+         ; never _ → <:-never })
 
     result₀ : LargestSrc F → Either (F ≮: (S ⇒ T)) (F <: (S ⇒ T))
     result₀ (defn S₀ T₀ o₀ T₀<:T src₀) with dec-src o₀
-    result₀ (defn S₀ T₀ o₀ T₀<:T src₀) | Right S<:S₀ = Right (ov-<: o₀ (<:-function S<:S₀ T₀<:T))
+    result₀ (defn S₀ T₀ o₀ T₀<:T src₀) | Right S<:S₀ = Right (ov-<: Fᶠ o₀ (<:-function S<:S₀ T₀<:T))
     result₀ (defn S₀ T₀ o₀ T₀<:T src₀) | Left (witness s Ss ¬S₀s) = Left (result₁ (smallest Fᶠ (λ o → o))) where
 
       data SmallestTgt (G : Type) : Set where
 
         defn : ∀ S₁ T₁ →
 
-          Overload F (S₁ ⇒ T₁) →
+          Overloads F (S₁ ⇒ T₁) →
           Language S₁ s →
-          (∀ {S′ T′} → Overload G (S′ ⇒ T′) → Language S′ s → (T₁ <: T′)) →
+          (∀ {S′ T′} → Overloads G (S′ ⇒ T′) → Language S′ s → (T₁ <: T′)) →
           -----------------------
           SmallestTgt G
 
       smallest : ∀ {G} → (FunType G) → (G ⊆ᵒ F) → SmallestTgt G
       smallest {S′ ⇒ T′} _ G⊆F with dec-language S′ s
-      smallest {S′ ⇒ T′} _ G⊆F | Left ¬S′s = defn Sᵗ Tᵗ oᵗ (S<:Sᵗ s Ss) λ { here S′s → CONTRADICTION (language-comp s ¬S′s S′s) }
+      smallest {S′ ⇒ T′} _ G⊆F | Left ¬S′s = defn Sᵗ Tᵗ oᵗ (S<:Sᵗ s Ss) λ { here S′s → CONTRADICTION (language-comp s ¬S′s S′s) ; never (scalar ()) }
-      smallest {S′ ⇒ T′} _ G⊆F | Right S′s = defn S′ T′ (G⊆F here) S′s (λ { here _ → <:-refl })
+      smallest {S′ ⇒ T′} _ G⊆F | Right S′s = defn S′ T′ (G⊆F here) S′s (λ { here _ → <:-refl ; never (scalar ()) })
       smallest (Gᶠ ∩ Hᶠ) GH⊆F with smallest Gᶠ (GH⊆F ∘ left) | smallest Hᶠ (GH⊆F ∘ right)
       smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ with sat-∩ o₁ o₂
       smallest (Gᶠ ∩ Hᶠ) GH⊆F | defn S₁ T₁ o₁ R₁s tgt₁ | defn S₂ T₂ o₂ R₂s tgt₂ | defn o src tgt = defn _ _ o (src s (R₁s , R₂s))
-        (λ { (left o) S′s → <:-trans (<:-trans tgt <:-∩-left) (tgt₁ o S′s) ; (right o) S′s → <:-trans (<:-trans tgt <:-∩-right) (tgt₂ o S′s)} )
+        (λ { (left o) S′s → <:-trans (<:-trans tgt <:-∩-left) (tgt₁ o S′s)
+           ; (right o) S′s → <:-trans (<:-trans tgt <:-∩-right) (tgt₂ o S′s)
+           ; never (scalar ()) } )
 
       result₁ : SmallestTgt F → (F ≮: (S ⇒ T))
       result₁ (defn S₁ T₁ o₁ S₁s tgt₁) with dec-tgt o₁
       result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Right T₁<:T = CONTRADICTION (language-comp s ¬S₀s (src₀ o₁ T₁<:T s S₁s))
       result₁ (defn S₁ T₁ o₁ S₁s tgt₁) | Left (witness t T₁t ¬Tt) = witness (function-ok s t) (ov-language Fᶠ lemma) (function-ok Ss ¬Tt) where
 
-        lemma : ∀ {S′ T′} → Overload F (S′ ⇒ T′) → Language (S′ ⇒ T′) (function-ok s t)
+        lemma : ∀ {S′ T′} → Overloads F (S′ ⇒ T′) → Language (S′ ⇒ T′) (function-ok s t)
         lemma {S′} o with dec-language S′ s
         lemma {S′} o | Left ¬S′s = function-ok₁ ¬S′s
         lemma {S′} o | Right S′s = function-ok₂ (tgt₁ o S′s t T₁t)