Cleanup Type properties.

4 files changed, 1035 insertions, 261 deletions

diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index b167933..40d569a 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -109,6 +109,7 @@ private
   ; trans = λ {e} {e′} {e′′} → ≈-trans {n} {e} {e′} {e′′}
   }
 
+------------------------------------------------------------------------
 -- Bundles
 
 partialSetoid : ∀ {n} → PartialSetoid _ _
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index 6248e76..13e5ab1 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -29,7 +29,7 @@ import Data.Nat as ℕ
 open import Data.Product as P
 open import Data.Sum as S
 open import Function hiding (_⟶_)
-open import Level renaming (suc to lsuc)
+open import Level
 import Relation.Binary.Construct.On as On
 open import Relation.Binary.PropositionalEquality hiding (setoid; [_])
 open import Relation.Nullary hiding (Irrelevant)
@@ -52,6 +52,14 @@ private
   w++[]≋w (x ∷ w) = ∼-refl ∷ w++[]≋w w
 
 ------------------------------------------------------------------------
+-- Properties of First
+------------------------------------------------------------------------
+
+First-resp-∼ : ∀ (A : Language a) {c c′} → c ∼ c′ → First A c → First A c′
+First-resp-∼ A c∼c′ (w , cw∈A) = w , ∈-resp-≋ (c∼c′ ∷ ≋-refl) cw∈A
+  where open Language A
+
+------------------------------------------------------------------------
 -- Properties of _⊆_
 ------------------------------------------------------------------------
 -- Relational properties of _⊆_
@@ -71,6 +79,9 @@ private
 ⊆-antisym : Antisym (_⊆_ {a} {b}) _⊆_ _≈_
 ⊆-antisym = _,_
 
+⊆-min : Min (_⊆_ {a} {b}) ∅
+⊆-min _ = sub λ ()
+
 ------------------------------------------------------------------------
 -- Membership properties of _⊆_
 
@@ -83,10 +94,10 @@ private
 Null-resp-⊆ : Null {a} ⟶ Null {b} Respects _⊆_
 Null-resp-⊆ = ∈-resp-⊆
 
-First-resp-⊆ : ∀ {c} → flip (First {a}) c ⟶ flip (First {a}) c Respects _⊆_
+First-resp-⊆ : ∀ {c} → flip (First {a}) c ⟶ flip (First {b}) c Respects _⊆_
 First-resp-⊆ (sub A⊆B) = P.map₂ A⊆B
 
-Flast-resp-⊆ : ∀ {c} → flip (Flast {a}) c ⟶ flip (Flast {a}) c Respects _⊆_
+Flast-resp-⊆ : ∀ {c} → flip (Flast {a}) c ⟶ flip (Flast {b}) c Respects _⊆_
 Flast-resp-⊆ (sub A⊆B) = P.map₂ (P.map₂ (P.map A⊆B (P.map₂ A⊆B)))
 
 ------------------------------------------------------------------------
@@ -108,43 +119,43 @@ Flast-resp-⊆ (sub A⊆B) = P.map₂ (P.map₂ (P.map A⊆B (P.map₂ A⊆B)))
 
 ≈-isPartialEquivalence : IsPartialEquivalence (_≈_ {a})
 ≈-isPartialEquivalence = record
-  { sym = ≈-sym
+  { sym   = ≈-sym
   ; trans = ≈-trans
   }
 
 ≈-isEquivalence : IsEquivalence (_≈_ {a})
 ≈-isEquivalence = record
-  { refl = ≈-refl
-  ; sym = ≈-sym
+  { refl  = ≈-refl
+  ; sym   = ≈-sym
   ; trans = ≈-trans
   }
 
 ⊆-isPreorder : IsPreorder (_≈_ {a}) _⊆_
 ⊆-isPreorder = record
   { isEquivalence = ≈-isEquivalence
-  ; reflexive = ⊆-reflexive
-  ; trans = ⊆-trans
+  ; reflexive     = ⊆-reflexive
+  ; trans         = ⊆-trans
   }
 
 ⊆-isPartialOrder : IsPartialOrder (_≈_ {a}) _⊆_
 ⊆-isPartialOrder = record
   { isPreorder = ⊆-isPreorder
-  ; antisym = ⊆-antisym
+  ; antisym    = ⊆-antisym
   }
 
 ------------------------------------------------------------------------
 -- Bundles
 
-partialSetoid : PartialSetoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+partialSetoid : ∀ {a} → PartialSetoid _ _
 partialSetoid {a} = record { isPartialEquivalence = ≈-isPartialEquivalence {a} }
 
-setoid : Setoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+setoid : ∀ {a} → Setoid _ _
 setoid {a} = record { isEquivalence = ≈-isEquivalence {a} }
 
-⊆-preorder : Preorder (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+⊆-preorder : ∀ {a} → Preorder _ _ _
 ⊆-preorder {a} = record { isPreorder = ⊆-isPreorder {a} }
 
-⊆-poset : Poset (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+⊆-poset : ∀ {a} → Poset _ _ _
 ⊆-poset {a} = record { isPartialOrder = ⊆-isPartialOrder {a} }
 
 ------------------------------------------------------------------------
@@ -159,10 +170,10 @@ setoid {a} = record { isEquivalence = ≈-isEquivalence {a} }
 Null-resp-≈ : Null {a} ⟶ Null {b} Respects _≈_
 Null-resp-≈ = Null-resp-⊆ ∘ ⊆-reflexive
 
-First-resp-≈ : ∀ {c} → flip (First {a}) c ⟶ flip (First {a}) c Respects _≈_
+First-resp-≈ : ∀ {c} → flip (First {a}) c ⟶ flip (First {b}) c Respects _≈_
 First-resp-≈ = First-resp-⊆ ∘ ⊆-reflexive
 
-Flast-resp-≈ : ∀ {c} → flip (Flast {a}) c ⟶ flip (Flast {a}) c Respects _≈_
+Flast-resp-≈ : ∀ {c} → flip (Flast {a}) c ⟶ flip (Flast {b}) c Respects _≈_
 Flast-resp-≈ = Flast-resp-⊆ ∘ ⊆-reflexive
 
 ------------------------------------------------------------------------
@@ -177,12 +188,6 @@ Recomputable-resp-≈ (sub A⊆B , sub A⊇B) recomp l∈B = A⊆B (recomp (A⊇
 ------------------------------------------------------------------------
 -- Properties of ∅
 ------------------------------------------------------------------------
--- Algebraic properties of ∅
-
-⊆-min : Min (_⊆_ {a} {b}) ∅
-⊆-min _ = sub λ ()
-
-------------------------------------------------------------------------
 -- Membership properties of ∅
 
 w∉∅ : ∀ w → w ∉ ∅ {a}
@@ -315,6 +320,13 @@ c∈First[A]+w′∈B⇒c∈First[A∙B] (_ , cw∈A) (_ , w′∈B) = -, -, -,
 ε∈A+c∈First[B]⇒c∈First[A∙B] : ∀ {c} → Null A → First B c → First (A ∙ B) c
 ε∈A+c∈First[B]⇒c∈First[A∙B] ε∈A (_ , cw∈B) = -, -, -, ε∈A , cw∈B , ≋-refl
 
+c∈First[A∙B]⇒c∈First[A]⊎ε∈A+c∈First[B] :
+  ∀ (A : Language a) (B : Language b) {c} → First (A ∙ B) c → First A c ⊎ Null A × First B c
+c∈First[A∙B]⇒c∈First[A]⊎ε∈A+c∈First[B] _ B (_ , []     , xw₂ , ε∈A   , xw₂∈B , x∼c ∷ _) =
+  inj₂ (ε∈A , First-resp-∼ B x∼c (-, xw₂∈B))
+c∈First[A∙B]⇒c∈First[A]⊎ε∈A+c∈First[B] A _ (_ , x ∷ w₁ , _   , xw₁∈A , _     , x∼c ∷ _) =
+  inj₁ (First-resp-∼ A x∼c (-, xw₁∈A))
+
 -- Flast
 
 c∈Flast[B]+w∈A⇒c∈Flast[A∙B] : ∀ {c} → Flast B c → ∃[ w ] w ∈ A → Flast (A ∙ B) c
@@ -406,6 +418,7 @@ c∈Flast[B]+w∈A⇒c∈Flast[A∙B] {c = c} (x , w , xw∈B , w′ , xwcw′�
 ∙-zero : (∀ (A : Language a) → ∅ {b} ∙ A ≈ ∅ {d}) × (∀ (A : Language a) → A ∙ ∅ {b} ≈ ∅ {d})
 ∙-zero = ∙-zeroˡ , ∙-zeroʳ
 
+------------------------------------------------------------------------
 -- Structures
 
 ∙-isMagma : ∀ {a} → IsMagma _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
@@ -426,15 +439,16 @@ c∈Flast[B]+w∈A⇒c∈Flast[A∙B] {c = c} (x , w , xw∈B , w′ , xwcw′�
   ; identity    = ∙-identity
   }
 
+------------------------------------------------------------------------
 -- Bundles
 
-∙-magma : ∀ {a} → Magma (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∙-magma : ∀ {a} → Magma _ _
 ∙-magma {a} = record { isMagma = ∙-isMagma {a} }
 
-∙-semigroup : ∀ {a} → Semigroup (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∙-semigroup : ∀ {a} → Semigroup _ _
 ∙-semigroup {a} = record { isSemigroup = ∙-isSemigroup {a} }
 
-∙-monoid : ∀ {a} → Monoid (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∙-monoid : ∀ {a} → Monoid _ _
 ∙-monoid {a} = record { isMonoid = ∙-isMonoid {a} }
 
 ------------------------------------------------------------------------
@@ -633,8 +647,9 @@ c∈Flast[B]⇒c∈Flast[A∪B] = P.map₂ (P.map₂ (P.map inj₂ (P.map₂ inj
 ∙-distrib-∪ = ∙-distribˡ-∪ , ∙-distribʳ-∪
 
 ∪-idem : ∀ (A : Language a) → A ∪ A ≈ A
-∪-idem A = ⊆-antisym (sub [ id , id ]′) (sub inj₁)
+∪-idem A = ⊆-antisym (sub reduce) (sub inj₁)
 
+------------------------------------------------------------------------
 -- Structures
 
 ∪-isMagma : IsMagma _≈_ (_∪_ {a})
@@ -720,46 +735,47 @@ c∈Flast[B]⇒c∈Flast[A∪B] = P.map₂ (P.map₂ (P.map inj₂ (P.map₂ inj
   ; zero                              = ∙-zero
   }
 
+------------------------------------------------------------------------
 -- Bundles
 
-∪-magma : Magma (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-magma : ∀ {a} → Magma _ _
 ∪-magma {a} = record { isMagma = ∪-isMagma {a} }
 
-∪-commutativeMagma : CommutativeMagma (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-commutativeMagma : ∀ {a} → CommutativeMagma _ _
 ∪-commutativeMagma {a} = record { isCommutativeMagma = ∪-isCommutativeMagma {a} }
 
-∪-semigroup : Semigroup (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-semigroup : ∀ {a} → Semigroup _ _
 ∪-semigroup {a} = record { isSemigroup = ∪-isSemigroup {a} }
 
-∪-band : Band (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-band : ∀ {a} → Band _ _
 ∪-band {a} = record { isBand = ∪-isBand {a} }
 
-∪-commutativeSemigroup : CommutativeSemigroup (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-commutativeSemigroup : ∀ {a} → CommutativeSemigroup _ _
 ∪-commutativeSemigroup {a} = record { isCommutativeSemigroup = ∪-isCommutativeSemigroup {a} }
 
-∪-semilattice : Semilattice (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-semilattice : ∀ {a} → Semilattice _ _
 ∪-semilattice {a} = record { isSemilattice = ∪-isSemilattice {a} }
 
-∪-monoid : Monoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-monoid : ∀ {a} → Monoid _ _
 ∪-monoid {a} = record { isMonoid = ∪-isMonoid {a} }
 
-∪-commutativeMonoid : CommutativeMonoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-commutativeMonoid : ∀ {a} → CommutativeMonoid _ _
 ∪-commutativeMonoid {a} = record { isCommutativeMonoid = ∪-isCommutativeMonoid {a} }
 
-∪-idempotentCommutativeMonoid : IdempotentCommutativeMonoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-idempotentCommutativeMonoid : ∀ {a} → IdempotentCommutativeMonoid _ _
 ∪-idempotentCommutativeMonoid {a} = record
   { isIdempotentCommutativeMonoid = ∪-isIdempotentCommutativeMonoid {a} }
 
-∪-∙-nearSemiring : NearSemiring (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∪-∙-nearSemiring : ∀ {a} → NearSemiring _ _
 ∪-∙-nearSemiring {a} = record { isNearSemiring = ∪-∙-isNearSemiring {a} }
 
-∪-∙-semiringWithoutOne : SemiringWithoutOne (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∪-∙-semiringWithoutOne : ∀ {a} → SemiringWithoutOne _ _
 ∪-∙-semiringWithoutOne {a} = record { isSemiringWithoutOne = ∪-∙-isSemiringWithoutOne {a} }
 
-∪-∙-semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∪-∙-semiringWithoutAnnihilatingZero : ∀ {a} → SemiringWithoutAnnihilatingZero _ _
 ∪-∙-semiringWithoutAnnihilatingZero {a} = record { isSemiringWithoutAnnihilatingZero = ∪-∙-isSemiringWithoutAnnihilatingZero {a} }
 
-∪-∙-semiring : Semiring (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∪-∙-semiring : ∀ {a} → Semiring _ _
 ∪-∙-semiring {a} = record { isSemiring = ∪-∙-isSemiring {a} }
 
 ------------------------------------------------------------------------
diff --git a/src/Cfe/Type/Base.agda b/src/Cfe/Type/Base.agda
index 98f7691..8e6603b 100644
--- a/src/Cfe/Type/Base.agda
+++ b/src/Cfe/Type/Base.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary using (_Respects_; Setoid)
+open import Relation.Binary using (REL; _Respects_; Setoid)
 
 module Cfe.Type.Base
   {c ℓ} (over : Setoid c ℓ)
@@ -13,7 +13,7 @@ open import Data.Bool renaming (_∨_ to _∨ᵇ_; _≤_ to _≤ᵇ_)
 open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product using (_×_)
 open import Data.Sum using (_⊎_; map)
-open import Function using (const; flip)
+open import Function
 open import Level
 open import Relation.Binary.PropositionalEquality using (_≡_)
 open import Relation.Nullary using (¬_)
@@ -22,23 +22,15 @@ private
   variable
     a b fℓ lℓ fℓ₁ lℓ₁ fℓ₂ lℓ₂ : Level
 
-  union : (C → Set a) → (C → Set b) → C → Set _
-  union A B c = A c ⊎ B c
-
-  union-cong :
-    ∀ {A : C → Set a} {B : C → Set b} →
-    A Respects _∼_ → B Respects _∼_ → union A B Respects _∼_
-  union-cong A-cong B-cong x∼y = map (A-cong x∼y) (B-cong x∼y)
-
-  if-cong :
-    ∀ {A B : C → Set a} cond →
-    A Respects _∼_ → B Respects _∼_ → (if cond then A else B) Respects _∼_
-  if-cong false A-cong B-cong = B-cong
-  if-cong true  A-cong B-cong = A-cong
-
 ------------------------------------------------------------------------
 -- Definitions
 
+infix 2 _⇒_
+
+_⇒_ : Bool → (C → Set a) → C → Set a
+false ⇒ A = const ⊥
+true  ⇒ A = A
+
 record Type fℓ lℓ : Set (c ⊔ ℓ ⊔ suc (fℓ ⊔ lℓ)) where
   field
     null       : Bool
@@ -86,11 +78,28 @@ infix 6 _∨_
 _∙_ : Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂)
 τ₁ ∙ τ₂ = record
   { null       = τ₁.null ∧ τ₂.null
-  ; first      = union τ₁.first (if τ₁.null then τ₂.first else const ⊥)
-  ; flast      = union τ₂.flast (if τ₂.null then union τ₂.first τ₁.flast else const ⊥)
-  ; first-cong = union-cong τ₁.first-cong (if-cong τ₁.null τ₂.first-cong (λ _ ()))
-  ; flast-cong =
-      union-cong τ₂.flast-cong (if-cong τ₂.null (union-cong τ₂.first-cong τ₁.flast-cong) (λ _ ()))
+  ; first      = λ c → τ₁.first c ⊎ (τ₁.null ⇒ τ₂.first) c
+  ; flast      = λ c → τ₂.flast c ⊎ (τ₂.null ⇒ λ c → τ₂.first c ⊎ τ₁.flast c) c
+  ; first-cong = λ {c} {c′} c∼c′ →
+      map
+        (τ₁.first-cong c∼c′)
+        (case τ₁.null
+         return (λ b → (b ⇒ τ₂.first) c → (b ⇒ τ₂.first) c′)
+         of λ
+           { true  → τ₂.first-cong c∼c′
+           ; false → id
+           })
+  ; flast-cong = λ {c} {c′} c∼c′ →
+      map
+        (τ₂.flast-cong c∼c′)
+        (case τ₂.null
+         return (λ b →
+           (b ⇒ λ c → τ₂.first c ⊎ τ₁.flast c) c →
+           (b ⇒ λ c → τ₂.first c ⊎ τ₁.flast c) c′)
+         of λ
+           { true  → map (τ₂.first-cong c∼c′) (τ₁.flast-cong c∼c′)
+           ; false → id
+           })
   }
   where
   module τ₁ = Type τ₁
@@ -99,10 +108,10 @@ _∙_ : Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ
 _∨_ : Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ lℓ₂)
 τ₁ ∨ τ₂ = record
   { null       = τ₁.null ∨ᵇ τ₂.null
-  ; first      = union τ₁.first τ₂.first
-  ; flast      = union τ₁.flast τ₂.flast
-  ; first-cong = union-cong τ₁.first-cong τ₂.first-cong
-  ; flast-cong = union-cong τ₁.flast-cong τ₂.flast-cong
+  ; first      = λ c → τ₁.first c ⊎ τ₂.first c
+  ; flast      = λ c → τ₁.flast c ⊎ τ₂.flast c
+  ; first-cong = λ c∼c′ → map (τ₁.first-cong c∼c′) (τ₂.first-cong c∼c′)
+  ; flast-cong = λ c∼c′ → map (τ₁.flast-cong c∼c′) (τ₂.flast-cong c∼c′)
   }
   where
   module τ₁ = Type τ₁
@@ -111,11 +120,7 @@ _∨_ : Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ
 ------------------------------------------------------------------------
 -- Relations
 
-infix 4 _≈_
-infix 4 _≤_
-infix 4 _⊨_
-infix 4 _⊛_
-infix 4 _#_
+infix 4 _≈_ _≤_ _≥_ _⊨_ _⊛_ _#_
 
 record _≈_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
   module τ₁ = Type τ₁
@@ -123,9 +128,9 @@ record _≈_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set
   field
     n≡n   : τ₁.null ≡ τ₂.null
     f₁⊆f₂ : ∀ {c} → τ₁.first c → τ₂.first c
-    f₁⊇f₂ : ∀ {c} → τ₁.first c → τ₂.first c
+    f₁⊇f₂ : ∀ {c} → τ₂.first c → τ₁.first c
     l₁⊆l₂ : ∀ {c} → τ₁.flast c → τ₂.flast c
-    l₁⊇l₂ : ∀ {c} → τ₁.flast c → τ₂.flast c
+    l₁⊇l₂ : ∀ {c} → τ₂.flast c → τ₁.flast c
 
 record _≤_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂) where
   module τ₁ = Type τ₁
@@ -135,6 +140,9 @@ record _≤_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set
     f⊆f : ∀ {c} → τ₁.first c → τ₂.first c
     l⊆l : ∀ {c} → τ₁.flast c → τ₂.flast c
 
+_≥_ : REL (Type fℓ₁ lℓ₁) (Type fℓ₂ lℓ₂) _
+_≥_ = flip _≤_
+
 record _⊨_ (A : Language a) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
   module τ = Type τ
   field
@@ -143,15 +151,17 @@ record _⊨_ (A : Language a) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔
     l⇒l : ∀ {c} → Flast A c → τ.flast c
 
 record _⊛_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ lℓ₁ ⊔ fℓ₂) where
-  module τ₁ = Type τ₁
-  module τ₂ = Type τ₂
+  private
+    module τ₁ = Type τ₁
+    module τ₂ = Type τ₂
   field
-    ∄[l₁∩f₂] : ∀ c → ¬ (τ₁.flast c × τ₂.first c)
+    ∄[l₁∩f₂] : ∀ {c} → ¬ (τ₁.flast c × τ₂.first c)
     ¬n₁      : ¬ T (τ₁.null)
 
 record _#_ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ fℓ₂) where
-  module τ₁ = Type τ₁
-  module τ₂ = Type τ₂
+  private
+    module τ₁ = Type τ₁
+    module τ₂ = Type τ₂
   field
-    ∄[f₁∩f₂] : ∀ c → ¬ (τ₁.first c × τ₂.first c)
+    ∄[f₁∩f₂] : ∀ {c} → ¬ (τ₁.first c × τ₂.first c)
     ¬n₁∨¬n₂  : ¬ (T τ₁.null × T τ₂.null)
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 2554ddd..29fa287 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -6,249 +6,996 @@ module Cfe.Type.Properties
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid over using () renaming (Carrier to C; _≈_ to _∼_)
+open Setoid over using ()
+  renaming
+  ( Carrier to C
+  ; _≈_ to _∼_
+  ; refl to ∼-refl
+  ; sym to ∼-sym
+  ; trans to ∼-trans
+  )
 
 open import Algebra
-open import Cfe.Language over renaming (_≤_ to _≤ˡ_; _≈_ to _≈ˡ_; ≤-min to ≤ˡ-min)
-open import Cfe.Language.Construct.Concatenate over renaming (_∙_ to _∙ˡ_)
-open import Cfe.Language.Construct.Single over
-open import Cfe.Language.Construct.Union over
-open import Cfe.Language.Indexed.Construct.Iterate over
+open import Cfe.Function.Power
+open import Cfe.Language over
+  hiding
+  ( _≉_; ≈-refl; ≈-trans; ≈-isPartialEquivalence; ≈-isEquivalence; partialSetoid; setoid
+  ; ∙-mono ; ∙-cong ; ∙-identityʳ ; ∙-assoc; ∙-isMagma ; ∙-isSemigroup ; ∙-magma ; ∙-semigroup )
+  renaming
+  ( _≈_ to _≈ˡ_
+  ; ≈-sym to ≈ˡ-sym
+  ; _∙_ to _∙ˡ_
+  )
+open import Cfe.List.Compare over
 open import Cfe.Type.Base over
+  renaming (_⇒_ to _⇒ᵗ_)
 open import Data.Bool renaming (_≤_ to _≤ᵇ_; _∨_ to _∨ᵇ_)
-open import Data.Bool.Properties hiding (≤-reflexive; ≤-trans)
-open import Data.Empty
-open import Data.List hiding (null)
-open import Data.List.Properties using (++-identityʳ; ++-assoc)
-open import Data.List.Relation.Binary.Equality.Setoid over
-open import Data.Nat hiding (_≤ᵇ_; _^_) renaming (_≤_ to _≤ⁿ_)
-open import Data.Nat.Properties using (≤-stepsˡ; ≤-stepsʳ) renaming (≤-refl to ≤ⁿ-refl)
-open import Data.Product as Product
-open import Data.Sum as Sum
-import Level as L
-open import Function hiding (_⟶_)
-import Relation.Unary as U
-open import Relation.Unary.Properties
-open import Relation.Binary.PropositionalEquality
-
-≤-min : ∀ {fℓ lℓ} → Min (_≤_ {_} {_} {fℓ} {lℓ}) τ⊥
-≤-min τ = record
-  { n≤n = ≤-minimum τ.Null
-  ; f⊆f = λ ()
-  ; l⊆l = λ ()
+open import Data.Bool.Properties
+  hiding
+    ( ≤-isPreorder; ≤-isPartialOrder ; ≤-preorder ; ≤-poset
+    ; ∨-identity
+    ; ∨-isMagma ; ∨-isSemigroup ; ∨-isBand ; ∨-isSemilattice ; ∨-isMonoid ; ∨-isCommutativeMonoid
+    ; ∨-isIdempotentCommutativeMonoid
+    ; ∨-magma ; ∨-semigroup ; ∨-band ; ∨-semilattice ; ∨-commutativeMonoid
+    ; ∨-idempotentCommutativeMonoid
+    )
+  renaming
+    ( ≤-refl to ≤ᵇ-refl
+    ; ≤-reflexive to ≤ᵇ-reflexive
+    ; ≤-trans to ≤ᵇ-trans
+    ; ≤-antisym to ≤ᵇ-antisym
+    ; ≤-maximum to ≤ᵇ-maximum
+    ; ≤-minimum to ≤ᵇ-minimum
+    ; ∨-assoc to ∨ᵇ-assoc
+    ; ∨-comm to ∨ᵇ-comm
+    ; ∨-identityˡ to ∨ᵇ-identityˡ
+    ; ∨-identityʳ to ∨ᵇ-identityʳ
+    ; ∨-idem to ∨ᵇ-idem
+    )
+open import Data.Empty using (⊥-elim)
+open import Data.Empty.Polymorphic using (⊥)
+open import Data.List using ([]; _∷_; _++_)
+open import Data.List.Properties using (++-assoc; ++-identityʳ)
+open import Data.List.Relation.Binary.Pointwise as Pw hiding (refl; setoid; map)
+open import Data.Nat using (suc; zero; _+_; z≤n; s≤s) renaming (_≤_ to _≤ⁿ_)
+open import Data.Nat.Properties using (m≤m+n; m≤n+m)
+open import Data.Product renaming (map to mapᵖ)
+open import Data.Product.Algebra using (×-distribˡ-⊎)
+open import Data.Sum hiding (map₁; map₂; swap)
+open import Function
+open import Function.Equality using (_⟨$⟩_)
+open import Function.Equivalence using (Equivalence)
+open import Level
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
+open import Relation.Nullary
+
+private
+  variable
+    a b fℓ lℓ fℓ₁ lℓ₁ fℓ₂ lℓ₂ fℓ₃ lℓ₃ fℓ₄ lℓ₄ : Level
+    A : Language a
+    B : Language b
+    τ : Type fℓ lℓ
+    τ₁ : Type fℓ₁ lℓ₁
+    τ₂ : Type fℓ₂ lℓ₂
+    τ₃ : Type fℓ₃ lℓ₃
+    τ₄ : Type fℓ₄ lℓ₄
+
+------------------------------------------------------------------------
+-- Miscellaneous properties
+------------------------------------------------------------------------
+-- T
+
+T-resp-≤ : T Respects _≤ᵇ_
+T-resp-≤ b≤b = id
+
+------------------------------------------------------------------------
+-- ∧
+
+∧-mono : Congruent₂ _≤ᵇ_ _∧_
+∧-mono {false} {v = false} f≤t u≤v = b≤b
+∧-mono {false} {v = false} b≤b u≤v = b≤b
+∧-mono {false} {v = true}  f≤t u≤v = f≤t
+∧-mono {false} {v = true}  b≤b u≤v = b≤b
+∧-mono {true}              b≤b u≤v = u≤v
+
+------------------------------------------------------------------------
+-- ∨ᵇ
+
+∨ᵇ-mono : Congruent₂ _≤ᵇ_ _∨ᵇ_
+∨ᵇ-mono {true}              b≤b u≤v = b≤b
+∨ᵇ-mono {false}             b≤b u≤v = u≤v
+∨ᵇ-mono {false} {u = false} f≤t u≤v = f≤t
+∨ᵇ-mono {false} {u = true}  f≤t u≤v = b≤b
+
+------------------------------------------------------------------------
+-- _⇒ᵗ_
+
+⇒ᵗ-mono :
+  ∀ {b₁ b₂} {A : C → Set a} {B : C → Set b} →
+  b₁ ≤ᵇ b₂ → (∀ {c} → A c → B c) → ∀ {c} → (b₁ ⇒ᵗ A) c → (b₂ ⇒ᵗ B) c
+⇒ᵗ-mono {b₁ = true} b≤b A⊆B c∈A = A⊆B c∈A
+
+⇒ᵗ-monoˡ :
+  ∀ {b₁ b₂} (A : C → Set a) →
+  b₁ ≤ᵇ b₂ → ∀ {c} → (b₁ ⇒ᵗ A) c → (b₂ ⇒ᵗ A) c
+⇒ᵗ-monoˡ A b₁≤b₂ = ⇒ᵗ-mono b₁≤b₂ id
+
+⇒ᵗ-monoʳ :
+  ∀ {A : C → Set a} {B : C → Set b} b → (∀ {c} → A c → B c) → ∀ {c} → (b ⇒ᵗ A) c → (b ⇒ᵗ B) c
+⇒ᵗ-monoʳ b A⊆B = ⇒ᵗ-mono (≤ᵇ-refl {b}) A⊆B
+
+⇒ᵗ-construct : ∀ {b} {A : C → Set a} {c} → T b → A c → (b ⇒ᵗ A) c
+⇒ᵗ-construct {b = true} _ c∈A = c∈A
+
+⇒ᵗ-zeroʳ : ∀ {A : C → Set a} b → (∀ {c} → ¬ A c) → ∀ {c} → ¬ (b ⇒ᵗ A) c
+⇒ᵗ-zeroʳ true ∄[A] c∈A = ∄[A] c∈A
+
+⇒ᵗ-idemˡ : ∀ b (A : C → Set a) {c} → (b ⇒ᵗ (b ⇒ᵗ A)) c → (b ⇒ᵗ A) c
+⇒ᵗ-idemˡ true _ c∈A = c∈A
+
+⇒ᵗA⊆A : ∀ b (A : C → Set a) {c} → (b ⇒ᵗ A) c → A c
+⇒ᵗA⊆A true _ c∈A = c∈A
+
+⇒ᵗ-⊎ : ∀ x (A : C → Set a) (B : C → Set b) {c} → (x ⇒ᵗ λ c → A c ⊎ B c) c → (x ⇒ᵗ A) c ⊎ (x ⇒ᵗ B) c
+⇒ᵗ-⊎ true _ _ c∈A⊎B = c∈A⊎B
+
+⇒ᵗ-∧ : ∀ b₁ b₂ (A : C → Set a) {c} → (b₁ ∧ b₂ ⇒ᵗ A) c → (b₁ ⇒ᵗ (b₂ ⇒ᵗ A)) c
+⇒ᵗ-∧ true true _ c∈A = c∈A
+
+⇒ᵗ-∧′ : ∀ b₁ b₂ (A : C → Set a) {c} → (b₁ ⇒ᵗ (b₂ ⇒ᵗ A)) c → (b₁ ∧ b₂ ⇒ᵗ A) c
+⇒ᵗ-∧′ true true _ c∈A = c∈A
+
+⇒ᵗ-∨ᵇ : ∀ b₁ b₂ (A : C → Set a) {c} → (b₁ ∨ᵇ b₂ ⇒ᵗ A) c → (b₁ ⇒ᵗ A) c ⊎ (b₂ ⇒ᵗ A) c
+⇒ᵗ-∨ᵇ true  _    _ c∈A = inj₁ c∈A
+⇒ᵗ-∨ᵇ false true _ c∈A = inj₂ c∈A
+
+⇒ᵗ-∨ᵇ′ˡ : ∀ b₁ b₂ (A : C → Set a) {c} → (b₁ ⇒ᵗ A) c → (b₁ ∨ᵇ b₂ ⇒ᵗ A) c
+⇒ᵗ-∨ᵇ′ˡ true _ _ c∈A = c∈A
+
+⇒ᵗ-∨ᵇ′ʳ : ∀ b₁ b₂ (A : C → Set a) {c} → (b₂ ⇒ᵗ A) c → (b₁ ∨ᵇ b₂ ⇒ᵗ A) c
+⇒ᵗ-∨ᵇ′ʳ false true _ c∈A = c∈A
+⇒ᵗ-∨ᵇ′ʳ true  true _ c∈A = c∈A
+
+⇒ᵗ-contra : ∀ b (A : C → Set a) {c} → (b ⇒ᵗ A) c → T b
+⇒ᵗ-contra true _ _ = _
+
+------------------------------------------------------------------------
+-- Properties of _≈_
+------------------------------------------------------------------------
+-- Definitions
+
+infix 4 _≉_
+
+_≉_ : REL (Type fℓ₁ lℓ₁) (Type fℓ₂ lℓ₂) _
+τ₁ ≉ τ₂ = ¬ τ₁ ≈ τ₂
+
+-- Relational Properties
+
+≈-refl : Reflexive (_≈_ {fℓ} {lℓ})
+≈-refl = record
+  { n≡n   = refl
+  ; f₁⊆f₂ = id
+  ; f₁⊇f₂ = id
+  ; l₁⊆l₂ = id
+  ; l₁⊇l₂ = id
+  }
+
+≈-sym : Sym (_≈_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂}) _≈_
+≈-sym τ₁≈τ₂ = record
+  { n≡n   = sym n≡n
+  ; f₁⊆f₂ = f₁⊇f₂
+  ; f₁⊇f₂ = f₁⊆f₂
+  ; l₁⊆l₂ = l₁⊇l₂
+  ; l₁⊇l₂ = l₁⊆l₂
+  }
+  where
+  open _≈_ τ₁≈τ₂
+
+≈-trans : Trans (_≈_ {fℓ₁} {lℓ₁}) (_≈_ {fℓ₂} {lℓ₂} {fℓ₃} {lℓ₃}) _≈_
+≈-trans τ₁≈τ₂ τ₂≈τ₃ = record
+  { n≡n   = trans τ₁≈τ₂.n≡n τ₂≈τ₃.n≡n
+  ; f₁⊆f₂ = τ₂≈τ₃.f₁⊆f₂ ∘ τ₁≈τ₂.f₁⊆f₂
+  ; f₁⊇f₂ = τ₁≈τ₂.f₁⊇f₂ ∘ τ₂≈τ₃.f₁⊇f₂
+  ; l₁⊆l₂ = τ₂≈τ₃.l₁⊆l₂ ∘ τ₁≈τ₂.l₁⊆l₂
+  ; l₁⊇l₂ = τ₁≈τ₂.l₁⊇l₂ ∘ τ₂≈τ₃.l₁⊇l₂
   }
   where
-  module τ = Type τ
+  module τ₁≈τ₂ = _≈_ τ₁≈τ₂
+  module τ₂≈τ₃ = _≈_ τ₂≈τ₃
+
+------------------------------------------------------------------------
+-- Structures
 
-L⊨τ+¬N⇒ε∉L : ∀ {a fℓ lℓ} {L : Language a} {τ : Type fℓ lℓ} → L ⊨ τ → T (not (Type.Null τ)) → [] ∉ L
-L⊨τ+¬N⇒ε∉L {L = L} {τ} L⊨τ ¬n ε∈L = case ∃[ b ] ((null L → T b) × T (not b)) ∋ Null τ , _⊨_.n⇒n L⊨τ , ¬n of λ
-  { (false , n⇒n , _) → n⇒n ε∈L }
+≈-isPartialEquivalence : IsPartialEquivalence (_≈_ {fℓ} {lℓ})
+≈-isPartialEquivalence = record
+  { sym   = ≈-sym
+  ; trans = ≈-trans
+  }
+
+≈-isEquivalence : IsEquivalence (_≈_ {fℓ} {lℓ})
+≈-isEquivalence = record
+  { refl  = ≈-refl
+  ; sym   = ≈-sym
+  ; trans = ≈-trans
+  }
+
+------------------------------------------------------------------------
+-- Bundles
+
+partialSetoid : ∀ {fℓ} {lℓ} → PartialSetoid _ _
+partialSetoid {fℓ} {lℓ} = record { isPartialEquivalence = ≈-isPartialEquivalence {fℓ} {lℓ} }
+
+setoid : ∀ {fℓ} {lℓ} → Setoid _ _
+setoid {fℓ} {lℓ} = record { isEquivalence = ≈-isEquivalence {fℓ} {lℓ} }
 
-⊨-anticongˡ : ∀ {a b fℓ lℓ} {A : Language a} {B : Language b} {τ : Type fℓ lℓ} → B ≤ˡ A → A ⊨ τ → B ⊨ τ
-⊨-anticongˡ B≤A A⊨τ = record
-  { n⇒n = A⊨τ.n⇒n ∘ B≤A.f
-  ; f⇒f = A⊨τ.f⇒f ∘ Product.map₂ B≤A.f
-  ; l⇒l = A⊨τ.l⇒l ∘ Product.map₂ (Product.map₂ (Product.map B≤A.f (Product.map₂ B≤A.f)))
+------------------------------------------------------------------------
+-- Properties of _≤_
+------------------------------------------------------------------------
+-- Relational Properties
+
+≤-refl : Reflexive (_≤_ {fℓ} {lℓ})
+≤-refl = record
+  { n≤n = ≤ᵇ-refl
+  ; f⊆f = id
+  ; l⊆l = id
+  }
+
+≤-reflexive : _≈_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} ⇒ _≤_
+≤-reflexive τ₁≈τ₂ = record
+  { n≤n = ≤ᵇ-reflexive n≡n
+  ; f⊆f = f₁⊆f₂
+  ; l⊆l = l₁⊆l₂
   }
   where
-  module B≤A = _≤ˡ_ B≤A
-  module A⊨τ = _⊨_ A⊨τ
+  open _≈_ τ₁≈τ₂
 
-⊨-congʳ : ∀ {a fℓ₁ lℓ₁ fℓ₂ lℓ₂} {A : Language a} → (A ⊨_) ⟶ (A ⊨_) Respects (_≤_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂})
-⊨-congʳ {A = A} τ₁≤τ₂ A⊨τ₁ = record
-  { n⇒n = λ ε∈A → case ∃[ b ] (null A → T b) × ∃[ b′ ] b ≤ᵇ b′ ∋ τ₁.Null , A⊨τ₁.n⇒n , τ₂.Null , n≤n return (λ (_ , _ , x , _) → T x) of λ
-    { (_ , _ , true , _) → _
-    ; (false , n⇒n , false , _) → n⇒n ε∈A
-    }
-  ; f⇒f = f⊆f ∘ A⊨τ₁.f⇒f
-  ; l⇒l = l⊆l ∘ A⊨τ₁.l⇒l
+≥-reflexive : _≈_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} ⇒ _≥_
+≥-reflexive τ₁≈τ₂ = record
+  { n≤n = ≤ᵇ-reflexive (sym n≡n)
+  ; f⊆f = f₁⊇f₂
+  ; l⊆l = l₁⊇l₂
   }
   where
-  open _≤_ τ₁≤τ₂
-  module A⊨τ₁ = _⊨_ A⊨τ₁
+  open _≈_ τ₁≈τ₂
 
-⊨-liftˡ : ∀ {a fℓ lℓ} {L : Language a} {τ : Type fℓ lℓ} b → L ⊨ τ → Lift b L ⊨ τ
-⊨-liftˡ _ L⊨τ = record
-  { n⇒n = λ { ( L.lift ε∈L ) → n⇒n ε∈L }
-  ; f⇒f = λ { ( l , L.lift xl∈L ) → f⇒f (-, xl∈L)}
-  ; l⇒l = λ { ( l , l≢[] , L.lift l∈L , l′ , L.lift lxl′∈L ) → l⇒l (-, l≢[] , l∈L , -, lxl′∈L)}
+≤-trans : Trans (_≤_ {fℓ₁} {lℓ₁}) (_≤_ {fℓ₂} {lℓ₂} {fℓ₃} {lℓ₃}) _≤_
+≤-trans τ₁≤τ₂ τ₂≤τ₃ = record
+  { n≤n = ≤ᵇ-trans τ₁≤τ₂.n≤n τ₂≤τ₃.n≤n
+  ; f⊆f = τ₂≤τ₃.f⊆f ∘ τ₁≤τ₂.f⊆f
+  ; l⊆l = τ₂≤τ₃.l⊆l ∘ τ₁≤τ₂.l⊆l
   }
   where
-  open _⊨_ L⊨τ
+  module τ₁≤τ₂ = _≤_ τ₁≤τ₂
+  module τ₂≤τ₃ = _≤_ τ₂≤τ₃
 
-L⊨τ⊥⇒L≈∅ : ∀ {a} {L : Language a} → L ⊨ τ⊥ → L ≈ˡ ∅
-L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
-  { f = λ {l} → elim l
-  ; f⁻¹ = λ ()
+≤-antisym : Antisym (_≤_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂}) _≤_ _≈_
+≤-antisym τ₁≤τ₂ τ₁≥τ₂ = record
+  { n≡n   = ≤ᵇ-antisym τ₁≤τ₂.n≤n τ₁≥τ₂.n≤n
+  ; f₁⊆f₂ = τ₁≤τ₂.f⊆f
+  ; f₁⊇f₂ = τ₁≥τ₂.f⊆f
+  ; l₁⊆l₂ = τ₁≤τ₂.l⊆l
+  ; l₁⊇l₂ = τ₁≥τ₂.l⊆l
   }
   where
-  module L⊨τ⊥ = _⊨_ L⊨τ⊥
+  module τ₁≤τ₂ = _≤_ τ₁≤τ₂
+  module τ₁≥τ₂ = _≤_ τ₁≥τ₂
 
-  elim : ∀ l (l∈L : l ∈ L) → l ∈ ∅
-  elim [] []∈L = L⊨τ⊥.n⇒n []∈L
-  elim (x ∷ l) xl∈L = L⊨τ⊥.f⇒f (-, xl∈L)
+≤-min : Min (_≤_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂}) τ⊥
+≤-min τ = record
+  { n≤n = ≤ᵇ-minimum null
+  ; f⊆f = λ ()
+  ; l⊆l = λ ()
+  }
+  where open Type τ
+
+------------------------------------------------------------------------
+-- Structures
+
+≤-isPreorder : IsPreorder (_≈_ {fℓ} {lℓ}) _≤_
+≤-isPreorder = record
+  { isEquivalence = ≈-isEquivalence
+  ; reflexive     = ≤-reflexive
+  ; trans         = ≤-trans
+  }
+
+≤-isPartialOrder : IsPartialOrder (_≈_ {fℓ} {lℓ}) _≤_
+≤-isPartialOrder = record
+  { isPreorder = ≤-isPreorder
+  ; antisym    = ≤-antisym
+  }
+
+------------------------------------------------------------------------
+-- Bundles
+
+≤-preorder : ∀ {fℓ} {lℓ} → Preorder _ _ _
+≤-preorder {fℓ} {lℓ} = record { isPreorder = ≤-isPreorder {fℓ} {lℓ} }
+
+≤-poset : ∀ {fℓ} {lℓ} → Poset _ _ _
+≤-poset {fℓ} {lℓ} = record { isPartialOrder = ≤-isPartialOrder {fℓ} {lℓ} }
 
-∅⊨τ⊥ : ∅ ⊨ τ⊥
-∅⊨τ⊥ = record
+------------------------------------------------------------------------
+-- Properties of _⊨_
+------------------------------------------------------------------------
+-- Relational Properties
+
+⊨-min : Min (_⊨_ {a} {fℓ} {lℓ}) ∅
+⊨-min τ = record
   { n⇒n = λ ()
   ; f⇒f = λ ()
   ; l⇒l = λ ()
   }
 
-L⊨τε⇒L≤｛ε｝ : ∀ {a} {L : Language a} → L ⊨ τε → L ≤ˡ ｛ε｝
-L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
-  { f = λ {l} → elim l
+⊨-resp-⊇ : A ⊇ B → A ⊨ τ → B ⊨ τ
+⊨-resp-⊇ A⊇B A⊨τ = record
+  { n⇒n = n⇒n ∘ Null-resp-⊆ A⊇B
+  ; f⇒f = f⇒f ∘ First-resp-⊆ A⊇B
+  ; l⇒l = l⇒l ∘ Flast-resp-⊆ A⊇B
+  }
+  where open _⊨_ A⊨τ
+
+⊨-resp-≈ˡ : A ≈ˡ B → A ⊨ τ → B ⊨ τ
+⊨-resp-≈ˡ = ⊨-resp-⊇ ∘ ⊇-reflexive
+
+⊨-resp-≤ : τ₁ ≤ τ₂ → A ⊨ τ₁ → A ⊨ τ₂
+⊨-resp-≤ τ₁≤τ₂ A⊨τ₁ = record
+  { n⇒n = T-resp-≤ n≤n ∘ n⇒n
+  ; f⇒f = f⊆f ∘ f⇒f
+  ; l⇒l = l⊆l ∘ l⇒l
+  }
+  where
+  open _≤_ τ₁≤τ₂
+  open _⊨_ A⊨τ₁
+
+⊨-resp-≈ʳ : τ₁ ≈ τ₂ → A ⊨ τ₁ → A ⊨ τ₂
+⊨-resp-≈ʳ = ⊨-resp-≤ ∘ ≤-reflexive
+
+⊨-fix : ∀ {F : Op₁ (Language a)} → Congruent₁ _⊆_ F → (∀ {A} → A ⊨ τ → F A ⊨ τ) → ⋃ F ⊨ τ
+⊨-fix {τ = τ} {F = F} mono ⊨-step = record
+  { n⇒n = uncurry Fⁿ⊨τ.n⇒n
+  ; f⇒f = λ (w , n , cw∈Fⁿ) → Fⁿ⊨τ.f⇒f n (-, cw∈Fⁿ)
+  ; l⇒l = λ (x , w , (m , xw∈Fᵐ) , w′ , n , xwcw′∈Fⁿ) →
+    Fⁿ⊨τ.l⇒l
+      (m + n)
+      (-, -, ∈-resp-⊆ (step (m≤m+n m n)) xw∈Fᵐ , -, ∈-resp-⊆ (step (m≤n+m n m)) xwcw′∈Fⁿ)
   }
   where
-  module L⊨τε = _⊨_ L⊨τε
+  Fⁿ⊨τ : ∀ n → (F ^ n) ∅ ⊨ τ
+  Fⁿ⊨τ zero    = ⊨-min τ
+  Fⁿ⊨τ (suc n) = ⊨-step (Fⁿ⊨τ n)
+
+  module Fⁿ⊨τ n = _⊨_ (Fⁿ⊨τ n)
+
+  step : ∀ {m n} → m ≤ⁿ n → (F ^ m) ∅ ⊆ (F ^ n) ∅
+  step {n = n} z≤n       = ⊆-min ((F  ^ n) ∅)
+  step         (s≤s m≤n) = mono (step m≤n)
+
+------------------------------------------------------------------------
+-- ⋃-⊨ : ∀ {a fℓ lℓ} {F : Op₁ (Language a)} {τ : Type fℓ lℓ} →
+--       (Congruent₁ _≤ˡ_ F) →
+--       (∀ {L} → L ⊨ τ → F L ⊨ τ) → ⋃ F ⊨ τ
+-- ⋃-⊨ {a} {F = F} {τ} ≤-mono ⊨-mono = record
+--   ; l⇒l = λ
+--     { (_ , l≢ε , (m , l∈Fᵐ) , _ , (n , l++x∷l′∈Fⁿ)) →
+--          _⊨_.l⇒l (Fⁿ⊨τ (m + n))
+--            (-, l≢ε , _≤ˡ_.f (^-mono (≤-stepsʳ {m} n ≤ⁿ-refl)) l∈Fᵐ ,
+--             -, _≤ˡ_.f (^-mono (≤-stepsˡ m ≤ⁿ-refl)) l++x∷l′∈Fⁿ)
+--     }
+--   }
+
+------------------------------------------------------------------------
+-- Properties of _⊛_
+------------------------------------------------------------------------
+
+⊛-resp-≥ˡ : τ₁ ≥ τ₂ → τ ⊛ τ₁ → τ ⊛ τ₂
+⊛-resp-≥ˡ τ₁≥τ₂ τ⊛τ₁ = record
+  { ∄[l₁∩f₂] = ∄[l₁∩f₂] ∘ map₂ f⊆f
+  ; ¬n₁      = ¬n₁
+  }
+  where
+  open _≤_ τ₁≥τ₂
+  open _⊛_ τ⊛τ₁
+
+⊛-resp-≥ʳ : τ₁ ≥ τ₂ → τ₁ ⊛ τ → τ₂ ⊛ τ
+⊛-resp-≥ʳ τ₁≥τ₂ τ₁⊛τ = record
+  { ∄[l₁∩f₂] = ∄[l₁∩f₂] ∘ map₁ l⊆l
+  ; ¬n₁      = ¬n₁ ∘ T-resp-≤ n≤n
+  }
+  where
+  open _≤_ τ₁≥τ₂
+  open _⊛_ τ₁⊛τ
+
+⊛-resp-≈ˡ : τ₁ ≈ τ₂ → τ ⊛ τ₁ → τ ⊛ τ₂
+⊛-resp-≈ˡ = ⊛-resp-≥ˡ ∘ ≥-reflexive
+
+⊛-resp-≈ʳ : τ₁ ≈ τ₂ → τ₁ ⊛ τ → τ₂ ⊛ τ
+⊛-resp-≈ʳ = ⊛-resp-≥ʳ ∘ ≥-reflexive
+
+------------------------------------------------------------------------
+-- Properties of _#_
+------------------------------------------------------------------------
+
+#-sym : Sym (_#_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂}) _#_
+#-sym τ₁#τ₂ = record
+  { ∄[f₁∩f₂] = ∄[f₁∩f₂] ∘ swap
+  ; ¬n₁∨¬n₂  = ¬n₁∨¬n₂ ∘ swap
+  }
+  where open _#_ τ₁#τ₂
+
+#-max : Max (_#_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂}) τ⊥
+#-max τ = record
+  { ∄[f₁∩f₂] = λ ()
+  ; ¬n₁∨¬n₂  = λ ()
+  }
+
+#-min : Min (_#_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂}) τ⊥
+#-min = #-sym ∘ #-max
+
+#-resp-≥ˡ : τ₁ ≥ τ₂ → τ # τ₁ → τ # τ₂
+#-resp-≥ˡ τ₁≥τ₂ τ#τ₁ = record
+  { ∄[f₁∩f₂] = ∄[f₁∩f₂] ∘ map₂ f⊆f
+  ; ¬n₁∨¬n₂  = ¬n₁∨¬n₂ ∘ map₂ (T-resp-≤ n≤n)
+  }
+  where
+  open _≤_ τ₁≥τ₂
+  open _#_ τ#τ₁
+
+#-resp-≥ʳ : τ₁ ≥ τ₂ → τ₁ # τ → τ₂ # τ
+#-resp-≥ʳ τ₁≥τ₂ τ₁#τ = record
+  { ∄[f₁∩f₂] = ∄[f₁∩f₂] ∘ map₁ f⊆f
+  ; ¬n₁∨¬n₂  = ¬n₁∨¬n₂ ∘ map₁ (T-resp-≤ n≤n)
+  }
+  where
+  open _≤_ τ₁≥τ₂
+  open _#_ τ₁#τ
+
+#-resp-≈ˡ : τ₁ ≈ τ₂ → τ # τ₁ → τ # τ₂
+#-resp-≈ˡ = #-resp-≥ˡ ∘ ≥-reflexive
+
+#-resp-≈ʳ : τ₁ ≈ τ₂ → τ₁ # τ → τ₂ # τ
+#-resp-≈ʳ = #-resp-≥ʳ ∘ ≥-reflexive
 
-  elim : ∀ l → l ∈ L → l ∈ ｛ε｝
-  elim [] []∈L = refl
-  elim (x ∷ l) xl∈L = ⊥-elim (L⊨τε.f⇒f (-, xl∈L))
+------------------------------------------------------------------------
+-- Properties of τ⊥
+------------------------------------------------------------------------
 
-｛ε｝⊨τε : ｛ε｝ ⊨ τε
+L⊨τ⊥⇒L≈∅ : A ⊨ τ⊥ {fℓ} {lℓ} → A ≈ˡ ∅ {b}
+L⊨τ⊥⇒L≈∅ {A = A} A⊨τ⊥ = ε∉A+∄[First[A]]⇒A≈∅ n⇒n (λ _ xw∈A → case f⇒f xw∈A of λ ())
+  where open _⊨_ A⊨τ⊥
+
+------------------------------------------------------------------------
+-- Properties of τε
+------------------------------------------------------------------------
+
+L⊨τε⇒L≤｛ε｝ : A ⊨ τε {fℓ} {lℓ} → A ⊆ ｛ε｝ {b}
+L⊨τε⇒L≤｛ε｝ {A = A} A⊨τε = ∄[First[A]]⇒A⊆｛ε｝ λ _ xw∈A → case f⇒f xw∈A of λ ()
+  where open _⊨_ A⊨τε
+
+｛ε｝⊨τε : ｛ε｝{a} ⊨ τε {fℓ} {lℓ}
 ｛ε｝⊨τε = record
-  { n⇒n = const tt
+  { n⇒n = const _
   ; f⇒f = λ ()
-  ; l⇒l = λ { ([] , ()) ; (_ ∷ _ , ())}
+  ; l⇒l = λ ()
   }
-  where
-  open import Data.Unit
+
+------------------------------------------------------------------------
+-- Properties of τ[_]
+------------------------------------------------------------------------
 
 ｛c｝⊨τ[c] : ∀ c → ｛ c ｝ ⊨ τ[ c ]
 ｛c｝⊨τ[c] c = record
   { n⇒n = λ ()
-  ; f⇒f = λ {x} → λ {([] , (c∼x ∷ []≋[])) → c∼x}
-  ; l⇒l = λ {x} → λ
-    { ([] , []≢[] , _) → ⊥-elim ([]≢[] refl)
-    ; (y ∷ [] , _ , _ , l′ , y∷x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y x l′ y∷x∷l′∈｛c｝)
-    ; (y ∷ z ∷ l , _ , _ , l′ , y∷z∷l++x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y z (l ++ x ∷ l′) y∷z∷l++x∷l′∈｛c｝)
-    }
+  ; f⇒f = λ {(_ , c∼c′ ∷ []) → c∼c′}
+  ; l⇒l = λ {(_ , [] , _ , [] , _ ∷ ())}
+  }
+
+------------------------------------------------------------------------
+-- Properties of _∙_
+------------------------------------------------------------------------
+-- Algebraic Properties
+
+∙-mono : τ₁ ≤ τ₂ → τ₃ ≤ τ₄ → τ₁ ∙ τ₃ ≤ τ₂ ∙ τ₄
+∙-mono τ₁≤τ₂ τ₃≤τ₄ = record
+  { n≤n = ∧-mono τ₁≤τ₂.n≤n τ₃≤τ₄.n≤n
+  ; f⊆f = map τ₁≤τ₂.f⊆f (⇒ᵗ-mono τ₁≤τ₂.n≤n τ₃≤τ₄.f⊆f)
+  ; l⊆l = map τ₃≤τ₄.l⊆l (⇒ᵗ-mono τ₃≤τ₄.n≤n (map τ₃≤τ₄.f⊆f τ₁≤τ₂.l⊆l))
+  }
+  where
+  module τ₁≤τ₂ = _≤_ τ₁≤τ₂
+  module τ₃≤τ₄ = _≤_ τ₃≤τ₄
+
+∙-cong : τ₁ ≈ τ₂ → τ₃ ≈ τ₄ → τ₁ ∙ τ₃ ≈ τ₂ ∙ τ₄
+∙-cong τ₁≈τ₂ τ₃≈τ₄ =
+  ≤-antisym
+    (∙-mono (≤-reflexive τ₁≈τ₂) (≤-reflexive τ₃≈τ₄))
+    (∙-mono (≤-reflexive (≈-sym τ₁≈τ₂)) (≤-reflexive (≈-sym τ₃≈τ₄)))
+
+∙-assoc :
+  ∀ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) (τ₃ : Type fℓ₃ lℓ₃) → (τ₁ ∙ τ₂) ∙ τ₃ ≈ τ₁ ∙ (τ₂ ∙ τ₃)
+∙-assoc τ₁ τ₂ τ₃ = record
+  { n≡n   = ∧-assoc τ₁.null τ₂.null τ₃.null
+  ; f₁⊆f₂ =
+    [ [ inj₁ , (inj₂ ∘ ⇒ᵗ-monoʳ τ₁.null inj₁) ]′
+    , inj₂ ∘ ⇒ᵗ-monoʳ τ₁.null inj₂ ∘ ⇒ᵗ-∧ τ₁.null τ₂.null τ₃.first
+    ]′
+  ; f₁⊇f₂ =
+    [ inj₁ ∘ inj₁
+    , [ inj₁ ∘ inj₂ , inj₂ ∘ ⇒ᵗ-∧′ τ₁.null τ₂.null τ₃.first ]′ ∘
+      ⇒ᵗ-⊎ τ₁.null τ₂.first (τ₂.null ⇒ᵗ τ₃.first)
+    ]′
+  ; l₁⊆l₂ =
+    [ inj₁ ∘ inj₁
+    , [ inj₁ ∘ inj₂ ∘ ⇒ᵗ-monoʳ τ₃.null inj₁
+      , [ inj₁ ∘ inj₂ ∘ ⇒ᵗ-monoʳ τ₃.null inj₂
+        , inj₂ ∘
+          ⇒ᵗ-mono (≤ᵇ-reflexive (∧-comm τ₃.null τ₂.null)) (map inj₁ id) ∘
+          ⇒ᵗ-∧′ τ₃.null τ₂.null (λ c → τ₂.first c ⊎ τ₁.flast c)
+        ]′ ∘
+        ⇒ᵗ-⊎ τ₃.null τ₂.flast (τ₂.null ⇒ᵗ λ c → τ₂.first c ⊎ τ₁.flast c)
+      ]′ ∘
+      ⇒ᵗ-⊎ τ₃.null τ₃.first (λ c → τ₂.flast c ⊎ (τ₂.null ⇒ᵗ λ c → τ₂.first c ⊎ τ₁.flast c) c)
+    ]′
+  ; l₁⊇l₂ =
+    [ [ inj₁
+      , inj₂ ∘
+        [ ⇒ᵗ-monoʳ τ₃.null inj₁
+        , ⇒ᵗ-monoʳ τ₃.null (inj₂ ∘ inj₁)
+        ]′ ∘
+        ⇒ᵗ-⊎ τ₃.null τ₃.first τ₂.flast
+      ]′
+    , inj₂ ∘
+      [ [ ⇒ᵗ-monoʳ τ₃.null (inj₂ ∘ inj₂) ∘
+          ⇒ᵗ-∧ τ₃.null τ₂.null (λ c → τ₂.first c ⊎ τ₁.flast c) ∘
+          ⇒ᵗ-mono (≤ᵇ-reflexive (∧-comm τ₂.null τ₃.null)) inj₁
+        , ⇒ᵗ-monoʳ τ₃.null (inj₁ ∘ ⇒ᵗA⊆A τ₂.null τ₃.first ∘ ⇒ᵗ-idemˡ τ₂.null τ₃.first) ∘
+          ⇒ᵗ-∧ τ₃.null τ₂.null (τ₂.null ⇒ᵗ τ₃.first) ∘
+          ⇒ᵗ-monoˡ (τ₂.null ⇒ᵗ τ₃.first) (≤ᵇ-reflexive (∧-comm τ₂.null τ₃.null))
+        ]′ ∘
+        ⇒ᵗ-⊎ (τ₂.null ∧ τ₃.null) τ₂.first (τ₂.null ⇒ᵗ τ₃.first)
+      , ⇒ᵗ-monoʳ τ₃.null (inj₂ ∘ inj₂) ∘
+        ⇒ᵗ-∧ τ₃.null τ₂.null (λ c → τ₂.first c ⊎ τ₁.flast c) ∘
+        ⇒ᵗ-mono (≤ᵇ-reflexive (∧-comm τ₂.null τ₃.null)) inj₂
+      ]′ ∘
+      ⇒ᵗ-⊎ (τ₂.null ∧ τ₃.null) (λ c → τ₂.first c ⊎ (τ₂.null ⇒ᵗ τ₃.first) c) τ₁.flast
+    ]′
+  }
+  where
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
+  module τ₃ = Type τ₃
+
+¬∙-identityˡ : C → Σ (Type ℓ lℓ₁) λ τ′ → (∀ (τ : Type fℓ₂ lℓ₂) → τ ∙ τ′ ≉ τ′)
+¬∙-identityˡ {fℓ₂ = fℓ₂} {lℓ₂} c = τ′ , go
+  where
+    τ′ = record
+      { null       = true
+      ; first      = c ∼_
+      ; flast      = const ⊥
+      ; first-cong = flip ∼-trans
+      ; flast-cong = λ _ ()
+      }
+
+    go : ∀ (τ : Type fℓ₂ lℓ₂) → τ ∙ τ′ ≉ τ′
+    go record { null = true } τ∙τ′≈τ′ = lower (l₁⊆l₂ (inj₂ (inj₁ ∼-refl)))
+      where open _≈_ τ∙τ′≈τ′
+
+∙-identityʳ : ∀ (τ : Type fℓ₁ lℓ₁) → τ ∙ τε {fℓ₂} {lℓ₂} ≈ τ
+∙-identityʳ τ = record
+  { n≡n   = ∧-identityʳ null
+  ; f₁⊆f₂ = [ id , ⊥-elim ∘ ⇒ᵗ-zeroʳ null (λ ()) ]′
+  ; f₁⊇f₂ = inj₁
+  ; l₁⊆l₂ = [ (λ ()) , [ (λ ()) , id ]′ ]′
+  ; l₁⊇l₂ = inj₂ ∘ inj₂
   }
+  where open Type τ
+
+¬∙-zeroˡ :
+  ∀ {c : C} (τ : Type fℓ₁ lℓ₁) → Dec (Type.flast τ c) → Σ (Type fℓ₂ (ℓ ⊔ lℓ₁)) λ τ′ → τ ∙ τ′ ≉ τ
+¬∙-zeroˡ {c = c} τ c∈?l = τ′ , go
   where
+    open Type τ
+    τ′ = record
+      { null       = false
+      ; first      = const ⊥
+      ; flast      = λ c′ → ¬ c ∼ c′ × flast c′ ⊎ c ∼ c′ × ¬ flast c′
+      ; first-cong = λ _ ()
+      ; flast-cong = λ
+        { x∼y (inj₁ (c≁x , x∈l)) → inj₁ (c≁x ∘ flip ∼-trans (∼-sym x∼y) , flast-cong x∼y x∈l)
+        ; x∼y (inj₂ (c∼x , x∉l)) → inj₂ (∼-trans c∼x x∼y , x∉l ∘ flast-cong (∼-sym x∼y))
+        }
+      }
+    go : τ ∙ τ′ ≉ τ
+    go τ∙τ′≈τ = case c∈?l of λ
+      { (yes c∈l) → [ [ (∼-refl |>_) ∘ proj₁ , (c∈l |>_) ∘ proj₂ ]′ , lower ]′ (l₁⊇l₂ c∈l)
+      ; (no c∉l)  → c∉l (l₁⊆l₂ (inj₁ (inj₂ (∼-refl , c∉l))))
+      }
+      where open _≈_ τ∙τ′≈τ
 
-∙-⊨ : ∀ {a b fℓ₁ lℓ₁ fℓ₂ lℓ₂} {A : Language a} {B : Language b} {τ₁ : Type fℓ₁ lℓ₁} {τ₂ : Type fℓ₂ lℓ₂} →
-      A ⊨ τ₁ → B ⊨ τ₂ → τ₁ ⊛ τ₂ → A ∙ˡ B ⊨ τ₁ ∙ τ₂
-∙-⊨ {A = A} {B} {τ₁} {τ₂} A⊨τ₁ B⊨τ₂ τ₁⊛τ₂ = record
-  { n⇒n = λ { record { l₁ = [] ; l₁∈A = ε∈A } → ⊥-elim (L⊨τ+¬N⇒ε∉L A⊨τ₁ τ₁⊛τ₂.¬n₁ ε∈A) }
-  ; f⇒f = λ
-    { (_ , record { l₁ = [] ; l₁∈A = ε∈A }) → ⊥-elim (L⊨τ+¬N⇒ε∉L A⊨τ₁ τ₁⊛τ₂.¬n₁ ε∈A)
-    ; (_ , record { l₁ = x ∷ l ; l₁∈A = xl∈A ; eq = x∼x ∷ _ }) → inj₁ (A⊨τ₁.f⇒f (l , A.∈-resp-≋ (x∼x ∷ ≋-refl) xl∈A))
+¬∙-zeroʳ :
+  ∀ {c : C} (τ : Type fℓ₁ lℓ₁) → Dec (Type.first τ c) → Σ (Type (ℓ ⊔ fℓ₁) lℓ₂) λ τ′ → τ′ ∙ τ ≉ τ
+¬∙-zeroʳ {c = c} τ c∈?f = τ′ , go
+  where
+    open Type τ
+    τ′ = record
+      { null       = false
+      ; first      = λ c′ → ¬ c ∼ c′ × first c′ ⊎ c ∼ c′ × ¬ first c′
+      ; flast      = const ⊥
+      ; first-cong = λ
+        { x∼y (inj₁ (c≁x , x∈l)) → inj₁ (c≁x ∘ flip ∼-trans (∼-sym x∼y) , first-cong x∼y x∈l)
+        ; x∼y (inj₂ (c∼x , x∉l)) → inj₂ (∼-trans c∼x x∼y , x∉l ∘ first-cong (∼-sym x∼y))
+        }
+      ; flast-cong = λ _ ()
+      }
+    go : τ′ ∙ τ ≉ τ
+    go τ′∙τ≈τ = case c∈?f of λ
+      { (yes c∈f) → [ [ (∼-refl |>_) ∘ proj₁ , (c∈f |>_) ∘ proj₂ ]′ , lower ]′ (f₁⊇f₂ c∈f)
+      ; (no c∉f)  → c∉f (f₁⊆f₂ (inj₁ (inj₂ (∼-refl , c∉f))))
+      }
+      where open _≈_ τ′∙τ≈τ
+
+∙-addˡ-⊛ˡ :
+  ∀ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) (τ₃ : Type fℓ₃ lℓ₃) → τ₂ ⊛ τ₃ → τ₁ ∙ τ₂ ⊛ τ₃
+∙-addˡ-⊛ˡ τ₁ τ₂ τ₃ τ₂⊛τ₃ = record
+  { ∄[l₁∩f₂] = λ
+    { (inj₁ c∈l₂   , c∈f₃) → ∄[l₂∩f₃] (c∈l₂ , c∈f₃)
+    ; (inj₂ c∈n₂⇒A , c∈f₃) → ¬n₂ (⇒ᵗ-contra τ₂.null (λ c → τ₂.first c ⊎ τ₁.flast c) c∈n₂⇒A)
     }
+  ; ¬n₁      = ¬n₂ ∘ proj₂ ∘ (Equivalence.to T-∧ ⟨$⟩_)
+  }
+  where
+  open _⊛_ τ₂⊛τ₃ using () renaming (∄[l₁∩f₂] to ∄[l₂∩f₃]; ¬n₁ to ¬n₂)
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
+
+∙-cancelʳ-⊛ʳ :
+  ∀ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) (τ₃ : Type fℓ₃ lℓ₃) → τ₁ ⊛ τ₂ ∙ τ₃ → τ₁ ⊛ τ₂
+∙-cancelʳ-⊛ʳ _ _ _ τ₁⊛τ₂∙τ₃ = record
+  { ∄[l₁∩f₂] = λ (c∈l₁ , c∈f₂) → ∄[l₁∩f₂] (c∈l₁ , inj₁ c∈f₂)
+  ; ¬n₁      = ¬n₁
+  }
+  where open _⊛_ τ₁⊛τ₂∙τ₃
+
+------------------------------------------------------------------------
+-- Structures
+
+∙-isMagma : ∀ {fℓ} {lℓ} → IsMagma _≈_ (_∙_ {fℓ} {fℓ ⊔ lℓ})
+∙-isMagma = record
+  { isEquivalence = ≈-isEquivalence
+  ; ∙-cong        = ∙-cong
+  }
+
+∙-isSemigroup : ∀ {fℓ} {lℓ} → IsSemigroup _≈_ (_∙_ {fℓ} {fℓ ⊔ lℓ})
+∙-isSemigroup {fℓ} {lℓ} = record
+  { isMagma = ∙-isMagma {fℓ} {lℓ}
+  ; assoc   = ∙-assoc
+  }
+
+------------------------------------------------------------------------
+-- Bundles
+
+∙-magma : ∀ {fℓ} {lℓ} → Magma _ _
+∙-magma {fℓ} {lℓ} = record { isMagma = ∙-isMagma {fℓ} {lℓ} }
+
+∙-semigroup : ∀ {fℓ} {lℓ} → Semigroup _ _
+∙-semigroup {fℓ} {lℓ} = record { isSemigroup = ∙-isSemigroup {fℓ} {lℓ} }
+
+------------------------------------------------------------------------
+-- Other properties
+
+⊛⇒∙-pres-⊨ : τ₁ ⊛ τ₂ → A ⊨ τ₁ → B ⊨ τ₂ → A ∙ˡ B ⊨ τ₁ ∙ τ₂
+⊛⇒∙-pres-⊨ {τ₁ = τ₁} {τ₂ = τ₂} {A = A} {B = B} τ₁⊛τ₂ A⊨τ₁ B⊨τ₂ = record
+  { n⇒n =  (Equivalence.from T-∧ ⟨$⟩_) ∘ < A⊨τ₁.n⇒n ∘ ε∈A∙B⇒ε∈A A B , B⊨τ₂.n⇒n ∘ ε∈A∙B⇒ε∈B A B >
+  ; f⇒f = λ c∈First[A∙B] →
+    map
+      A⊨τ₁.f⇒f
+      (uncurry ⇒ᵗ-construct ∘ mapᵖ A⊨τ₁.n⇒n B⊨τ₂.f⇒f)
+      (c∈First[A∙B]⇒c∈First[A]⊎ε∈A+c∈First[B] A B c∈First[A∙B])
   ; l⇒l = l⇒l
   }
   where
+  module ≋-setoid = Setoid (Pw.setoid over)
+  open import Relation.Binary.Reasoning.Setoid (Pw.setoid over)
+  open _⊛_ τ₁⊛τ₂
   module A = Language A
   module B = Language B
   module A⊨τ₁ = _⊨_ A⊨τ₁
   module B⊨τ₂ = _⊨_ B⊨τ₂
-  module τ₁⊛τ₂ = _⊛_ τ₁⊛τ₂
-
-  null-case : ∀ {c} → null B → Flast τ₂ c ⊎ First τ₂ c ⊎ Flast τ₁ c → Flast (τ₁ ∙ τ₂) c
-  null-case {c} ε∈B proof = case ∃[ b ] (null B → T b) ∋ Null τ₂ , B⊨τ₂.n⇒n return (λ (b , _) → (Flast τ₂ U.∪ (if b then _ else _)) c) of λ
-    { (false , n⇒n) → ⊥-elim (n⇒n ε∈B)
-    ; (true , _) → proof
-    }
 
-  l⇒l : flast (A ∙ˡ B) U.⊆ Flast (τ₁ ∙ τ₂)
-  l⇒l {c} (l , l≢ε , l∈A∙B @ record {l₂ = l₂} , l′ , lcl′∈A∙B) with Compare.compare
-    (Concat.l₁ l∈A∙B)
-    (Concat.l₂ l∈A∙B ++ c ∷ l′)
-    (Concat.l₁ lcl′∈A∙B)
-    (Concat.l₂ lcl′∈A∙B)
-    (begin
-      Concat.l₁ l∈A∙B ++ Concat.l₂ l∈A∙B ++ c ∷ l′   ≡˘⟨ ++-assoc (Concat.l₁ l∈A∙B) (Concat.l₂ l∈A∙B) (c ∷ l′) ⟩
-      (Concat.l₁ l∈A∙B ++ Concat.l₂ l∈A∙B) ++ c ∷ l′ ≈⟨ ++⁺ (Concat.eq l∈A∙B) ≋-refl ⟩
-      l ++ c ∷ l′                                    ≈˘⟨ Concat.eq lcl′∈A∙B ⟩
-      Concat.l₁ lcl′∈A∙B ++ Concat.l₂ lcl′∈A∙B        ∎)
+  l⇒l : ∀ {c} → Flast (A ∙ˡ B) c → Type.flast (τ₁ ∙ τ₂) c
+  l⇒l (_ , _ , _ , _ , [] , _ , ε∈A , _) = ⊥-elim (¬n₁ (A⊨τ₁.n⇒n ε∈A))
+  l⇒l (_ , _ , ([] , _ , ε∈A , _) , _ , _ ∷ _ , _)   = ⊥-elim (¬n₁ (A⊨τ₁.n⇒n ε∈A))
+  l⇒l {c} (x , w , (y ∷ w₁ , w₂ , yw₁∈A , w₂∈B , eq₁) , w′ , z ∷ w₁′ , w₂′ , zw₁′∈A , w₂′∈B , eq₂) with
+    compare (y ∷ w₁) (w₂ ++ c ∷ w′) (z ∷ w₁′) w₂′ (begin
+        y ∷ w₁ ++ w₂ ++ c ∷ w′   ≡˘⟨ ++-assoc (y ∷ w₁) w₂ (c ∷ w′) ⟩
+        (y ∷ w₁ ++ w₂) ++ c ∷ w′ ≈⟨ ++⁺ eq₁ (Pw.refl ∼-refl) ⟩
+        x ∷ w ++ c ∷ w′          ≈˘⟨ eq₂ ⟩
+        (z ∷ w₁′) ++ w₂′         ∎)
+  ... | cmp with <?> cmp
+  ... | tri< l _ _ =
+    ⊥-elim (∄[l₁∩f₂]
+      ( A⊨τ₁.l⇒l (-, -, zw₁′∈A , -, A.∈-resp-≋ w₁≋zw₁′cw′′ yw₁∈A)
+      , B⊨τ₂.f⇒f (-, B.∈-resp-≋ w₂′≋yw′′′ w₂′∈B)
+      ))
     where
-    open import Relation.Binary.Reasoning.Setoid ≋-setoid
-  ... | cmp with Compare.<?> cmp
-  ... | tri< x _ _ = ⊥-elim (τ₁⊛τ₂.∄[l₁∩f₂] y (A⊨τ₁.l⇒l (-, l₁′≢ε , Concat.l₁∈A lcl′∈A∙B , -, l₁′yw∈A) , B⊨τ₂.f⇒f (-, yw′∈B)))
+    lsplit      = left-split cmp l
+    w₁≋zw₁′cw′′ = proj₁ (proj₂ (proj₂ lsplit))
+    w₂′≋yw′′′   = ≋-setoid.sym (proj₂ (proj₂ (proj₂ lsplit)))
+  l⇒l {c} (_ , _ , (_ ∷ _ , [] , w₁∈A , ε∈B , _) , w′ , z ∷ w₁′ , [] , zw₁′∈A , _) | cmp | tri≈ _ e _ =
+    inj₂ (⇒ᵗ-construct
+      (B⊨τ₂.n⇒n ε∈B)
+      (inj₂ (A⊨τ₁.l⇒l (-, -, A.∈-resp-≋ w₁≋zw₁′ w₁∈A , -, A.∈-resp-≋ zw₁′≋zw₁′cw′ zw₁′∈A))))
     where
-    lsplit = Compare.left-split cmp x
-    y = proj₁ lsplit
-    l₁′≢ε = λ { refl → case ∃[ b ] T (not b) × (null A → T b) ∋ Null τ₁ , τ₁⊛τ₂.¬n₁ , A⊨τ₁.n⇒n of λ
-      { (false , _ , n⇒n) → n⇒n (Concat.l₁∈A lcl′∈A∙B)
-      ; (true , ¬n₁ , _) → ¬n₁
-      } }
-    l₁′yw∈A = A.∈-resp-≋ (proj₁ (proj₂ (proj₂ lsplit))) (Concat.l₁∈A l∈A∙B)
-    yw′∈B = B.∈-resp-≋ (≋-sym (proj₂ (proj₂ (proj₂ lsplit)))) (Concat.l₂∈B lcl′∈A∙B)
-  l⇒l {c} (l , l≢ε , l∈A∙B @ record { l₂ = [] } , l′ , lcl′∈A∙B) | cmp | tri≈ _ x _ =
-    null-case (Concat.l₂∈B l∈A∙B) (inj₂ (inj₁ (B⊨τ₂.f⇒f (-, cl′∈B))))
+    esplit = eq-split cmp e
+    w₁≋zw₁′ = proj₁ esplit
+    zw₁′≋zw₁′cw′ = begin
+      z ∷ w₁′           ≡˘⟨ ++-identityʳ (z ∷ w₁′) ⟩
+      z ∷ w₁′ ++ []     ≈˘⟨ ++⁺ (Pw.refl ∼-refl) (proj₂ esplit) ⟩
+      z ∷ w₁′ ++ c ∷ w′ ∎
+  l⇒l (_ , _ , (_ ∷ _ , [] , _ , ε∈B , _) , _ , _ ∷ _ , y ∷ w₂′ , _ , yw₂′∈B , _) | cmp | tri≈ _ e _ =
+    inj₂ (⇒ᵗ-construct (B⊨τ₂.n⇒n ε∈B) (inj₁ (B⊨τ₂.f⇒f (-, B.∈-resp-≋ yw₂′≋cw′ yw₂′∈B))))
     where
-    esplit = Compare.eq-split cmp x
-    cl′∈B = B.∈-resp-≋ (≋-sym (proj₂ esplit)) (Concat.l₂∈B lcl′∈A∙B)
-  l⇒l {c} (l , l≢ε , l∈A∙B @ record { l₂ = _ ∷ _ } , l′ , lcl′∈A∙B) | cmp | tri≈ _ x _ =
-    inj₁ (B⊨τ₂.l⇒l (-, (λ ()) , Concat.l₂∈B l∈A∙B , -, l₂cl′∈A∙B))
+    esplit = eq-split cmp e
+    yw₂′≋cw′ = ≋-setoid.sym (proj₂ esplit)
+  l⇒l {c} (_ , _ , (_ ∷ _ , _ ∷ _ , _ , yw₂∈B , _) , _ , _ ∷ _ , _ , _ , w₂′∈B , _) | cmp | tri≈ _ e _ =
+    inj₁ (B⊨τ₂.l⇒l (-, -, yw₂∈B , -, B.∈-resp-≋ w₂′≋yw₂cw′ w₂′∈B))
     where
-    esplit = Compare.eq-split cmp x
-    l₂cl′∈A∙B = B.∈-resp-≋ (≋-sym (proj₂ esplit)) (Concat.l₂∈B lcl′∈A∙B)
-  l⇒l {c} (l , l≢ε , l∈A∙B @ record { l₂ = [] } , l′ , lcl′∈A∙B) | cmp | tri> _ _ x =
-    null-case (Concat.l₂∈B l∈A∙B) (inj₂ (inj₂ (A⊨τ₁.l⇒l (-, l≢ε , l∈A , -, lcw∈A))))
+    esplit = eq-split cmp e
+    w₂′≋yw₂cw′ = ≋-setoid.sym (proj₂ esplit)
+  l⇒l {c} (x , w , (y ∷ w₁ , [] , yw₁∈A , ε∈B , eq₁) , w′ , z ∷ w₁′ , w₂′ , zw₁′∈A , w₂′∈B , eq₂) | cmp | tri> _ _ r =
+    inj₂ (⇒ᵗ-construct
+      (B⊨τ₂.n⇒n ε∈B)
+      (inj₂ (A⊨τ₁.l⇒l (-, -, A.∈-resp-≋ yw₁≋xw yw₁∈A , -, A.∈-resp-≋ zw₁′≋xwcw′′ zw₁′∈A))))
     where
-    rsplit = Compare.right-split cmp x
-    c∼y = case proj₂ (proj₂ (proj₂ rsplit)) of λ { (c∼y ∷ _) → c∼y }
-    l₁≋l = ≋-trans (≋-sym (≋-reflexive (++-identityʳ (Concat.l₁ l∈A∙B)))) (Concat.eq l∈A∙B)
-    lcw≋l₁yw = ≋-sym (≋-trans (++⁺ (≋-sym l₁≋l) (c∼y ∷ ≋-refl)) (proj₁ (proj₂ (proj₂ rsplit))))
-    l∈A = A.∈-resp-≋ l₁≋l (Concat.l₁∈A l∈A∙B)
-    lcw∈A = A.∈-resp-≋ lcw≋l₁yw (Concat.l₁∈A lcl′∈A∙B)
-  l⇒l {c} (l , l≢ε , l∈A∙B @ record { l₂ = y ∷ _ } , l′ , lcl′∈A∙B) | cmp | tri> _ _ x =
-    ⊥-elim (τ₁⊛τ₂.∄[l₁∩f₂] y (A⊨τ₁.l⇒l (-, l₁≢ε , Concat.l₁∈A l∈A∙B , -, l₁yw∈A) , B⊨τ₂.f⇒f (-, Concat.l₂∈B l∈A∙B)))
+    rsplit = right-split cmp r
+    c′ = proj₁ rsplit
+    w′′ = proj₁ (proj₂ rsplit)
+    c∼c′ = case proj₂ (proj₂ (proj₂ rsplit)) of λ {(c∼c′ ∷ _) → c∼c′}
+    yw₁≋xw = begin
+      y ∷ w₁       ≡˘⟨ ++-identityʳ (y ∷ w₁) ⟩
+      y ∷ w₁ ++ [] ≈⟨ eq₁ ⟩
+      x ∷ w        ∎
+    zw₁′≋xwcw′′ = begin
+      z ∷ w₁′            ≈˘⟨ proj₁ (proj₂ (proj₂ rsplit)) ⟩
+      y ∷ w₁ ++ c′ ∷ w′′ ≈⟨ ++⁺ yw₁≋xw (∼-sym c∼c′ ∷ Pw.refl ∼-refl) ⟩
+      x ∷ w ++ c ∷ w′′ ∎
+  l⇒l {c} (x , w , (y ∷ w₁ , y′ ∷ w₂ , yw₁∈A , y′w₂∈B , eq₁) , w′ , z ∷ w₁′ , w₂′ , zw₁′∈A , w₂′∈B , eq₂) | cmp | tri> _ _ r =
+    ⊥-elim (∄[l₁∩f₂]
+      ( A⊨τ₁.l⇒l (-, -, yw₁∈A , -, A.∈-resp-≋ zw₁′≋yw₁y′w′′ zw₁′∈A)
+      , B⊨τ₂.f⇒f (-, y′w₂∈B)
+      ))
     where
-    rsplit = Compare.right-split cmp x
-    l₁≢ε = λ { refl → case ∃[ b ] T (not b) × (null A → T b) ∋ Null τ₁ , τ₁⊛τ₂.¬n₁ , A⊨τ₁.n⇒n of λ
-      { (false , _ , n⇒n) → n⇒n (Concat.l₁∈A l∈A∙B)
-      ; (true , ¬n₁ , _) → ¬n₁
-      } }
-    y∼z = case proj₂ (proj₂ (proj₂ rsplit)) of λ { (y∼z ∷ _) → y∼z }
-    l₁′≋l₁yw = ≋-sym (≋-trans (++⁺ ≋-refl (y∼z ∷ ≋-refl)) (proj₁ (proj₂ (proj₂ rsplit))))
-    l₁yw∈A = A.∈-resp-≋ l₁′≋l₁yw (Concat.l₁∈A lcl′∈A∙B)
-
-∪-⊨ : ∀ {a b fℓ₁ lℓ₁ fℓ₂ lℓ₂} {A : Language a} {B : Language b} {τ₁ : Type fℓ₁ lℓ₁} {τ₂ : Type fℓ₂ lℓ₂} →
-      A ⊨ τ₁ → B ⊨ τ₂ → τ₁ # τ₂ → A ∪ B ⊨ τ₁ ∨ τ₂
-∪-⊨ {A = A} {B} {τ₁} {τ₂} A⊨τ₁ B⊨τ₂ τ₁#τ₂ = record
-  { n⇒n = λ
-    { (inj₁ ε∈A) → case ∃[ b ] T b ∋ Null τ₁ , A⊨τ₁.n⇒n ε∈A return (λ {(x , _) → T (x ∨ᵇ Null τ₂)}) of λ
-      { (true , _) → _ }
-    ; (inj₂ ε∈B) → case ∃[ b ] T b ∋ Null τ₂ , B⊨τ₂.n⇒n ε∈B return (λ {(x , _) → T (Null τ₁ ∨ᵇ x)}) of λ
-      { (true , _) → subst T (sym (∨-zeroʳ (Null τ₁))) _ }
-    }
-  ; f⇒f = λ
-    { (l , inj₁ x∷l∈A) → inj₁ (A⊨τ₁.f⇒f (-, x∷l∈A))
-    ; (l , inj₂ x∷l∈B) → inj₂ (B⊨τ₂.f⇒f (-, x∷l∈B))
-    }
-  ; l⇒l = λ
-    { ([] , l≢ε , l∈A∪B , l′ , l++x∷l′∈A∪B) → ⊥-elim (l≢ε refl)
-    ; (_ ∷ _ , _ , inj₁ l∈A , _ , inj₁ l++x∷l′∈A) → inj₁ (A⊨τ₁.l⇒l (-, (λ ()) , l∈A , -, l++x∷l′∈A))
-    ; (c ∷ _ , _ , inj₁ c∷u∈A , l′ , inj₂ c∷v∈B) → ⊥-elim (τ₁#τ₂.∄[f₁∩f₂] c (A⊨τ₁.f⇒f (-, c∷u∈A) , B⊨τ₂.f⇒f (-, c∷v∈B)))
-    ; (c ∷ _ , _ , inj₂ c∷u∈B , l′ , inj₁ c∷v∈A) → ⊥-elim (τ₁#τ₂.∄[f₁∩f₂] c (A⊨τ₁.f⇒f (-, c∷v∈A) , B⊨τ₂.f⇒f (-, c∷u∈B)))
-    ; (_ ∷ _ , _ , inj₂ l∈B , _ , inj₂ l++x∷l′∈B) → inj₂ (B⊨τ₂.l⇒l (-, (λ ()) , l∈B , -, l++x∷l′∈B))
-    }
+    rsplit = right-split cmp r
+    u = proj₁ rsplit
+    w′′ = proj₁ (proj₂ rsplit)
+    y′∼u = case (proj₂ (proj₂ (proj₂ rsplit))) of λ {(y′∼u ∷ _) → y′∼u}
+    zw₁′≋yw₁y′w′′ = begin
+      z ∷ w₁′            ≈˘⟨ proj₁ (proj₂ (proj₂ rsplit)) ⟩
+      y ∷ w₁ ++ u ∷ w′′  ≈˘⟨ ++⁺ (∼-refl ∷ Pw.refl ∼-refl) (y′∼u ∷ Pw.refl ∼-refl) ⟩
+      y ∷ w₁ ++ y′ ∷ w′′ ∎
+
+------------------------------------------------------------------------
+-- Properties of _∨_
+------------------------------------------------------------------------
+-- Algebraic Properties
+
+∨-mono : τ₁ ≤ τ₂ → τ₃ ≤ τ₄ → τ₁ ∨ τ₃ ≤ τ₂ ∨ τ₄
+∨-mono τ₁≤τ₂ τ₃≤τ₄ = record
+  { n≤n = ∨ᵇ-mono τ₁≤τ₂.n≤n τ₃≤τ₄.n≤n
+  ; f⊆f = map τ₁≤τ₂.f⊆f τ₃≤τ₄.f⊆f
+  ; l⊆l = map τ₁≤τ₂.l⊆l τ₃≤τ₄.l⊆l
   }
   where
-  module τ₁#τ₂ = _#_ τ₁#τ₂
-  module A⊨τ₁ = _⊨_ A⊨τ₁
-  module B⊨τ₂ = _⊨_ B⊨τ₂
+  module τ₁≤τ₂ = _≤_ τ₁≤τ₂
+  module τ₃≤τ₄ = _≤_ τ₃≤τ₄
 
-⋃-⊨ : ∀ {a fℓ lℓ} {F : Op₁ (Language a)} {τ : Type fℓ lℓ} →
-      (Congruent₁ _≤ˡ_ F) →
-      (∀ {L} → L ⊨ τ → F L ⊨ τ) → ⋃ F ⊨ τ
-⋃-⊨ {a} {F = F} {τ} ≤-mono ⊨-mono = record
-  { n⇒n = λ { (n , l∈Fⁿ) → _⊨_.n⇒n (Fⁿ⊨τ n) l∈Fⁿ}
-  ; f⇒f = λ { (_ , n , x∷l∈Fⁿ) → _⊨_.f⇒f (Fⁿ⊨τ n) (-, x∷l∈Fⁿ) }
-  ; l⇒l = λ
-    { (_ , l≢ε , (m , l∈Fᵐ) , _ , (n , l++x∷l′∈Fⁿ)) →
-         _⊨_.l⇒l (Fⁿ⊨τ (m + n))
-           (-, l≢ε , _≤ˡ_.f (^-mono (≤-stepsʳ {m} n ≤ⁿ-refl)) l∈Fᵐ ,
-            -, _≤ˡ_.f (^-mono (≤-stepsˡ m ≤ⁿ-refl)) l++x∷l′∈Fⁿ)
-    }
+∨-cong : τ₁ ≈ τ₂ → τ₃ ≈ τ₄ → τ₁ ∨ τ₃ ≈ τ₂ ∨ τ₄
+∨-cong τ₁≈τ₂ τ₃≈τ₄ =
+  ≤-antisym
+    (∨-mono (≤-reflexive τ₁≈τ₂) (≤-reflexive τ₃≈τ₄))
+    (∨-mono (≤-reflexive (≈-sym τ₁≈τ₂)) (≤-reflexive (≈-sym τ₃≈τ₄)))
+
+∨-assoc :
+  ∀ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) (τ₃ : Type fℓ₃ lℓ₃) → (τ₁ ∨ τ₂) ∨ τ₃ ≈ τ₁ ∨ (τ₂ ∨ τ₃)
+∨-assoc τ₁ τ₂ τ₃ = record
+  { n≡n   = ∨ᵇ-assoc τ₁.null τ₂.null τ₃.null
+  ; f₁⊆f₂ = [ [ inj₁ , inj₂ ∘ inj₁ ]′ , inj₂ ∘ inj₂ ]′
+  ; f₁⊇f₂ = [ inj₁ ∘ inj₁ , [ inj₁ ∘ inj₂ , inj₂ ]′ ]′
+  ; l₁⊆l₂ = [ [ inj₁ , inj₂ ∘ inj₁ ]′ , inj₂ ∘ inj₂ ]′
+  ; l₁⊇l₂ = [ inj₁ ∘ inj₁ , [ inj₁ ∘ inj₂ , inj₂ ]′ ]′
   }
   where
-  Fⁿ⊨τ : ∀ n → (F ^ n) (Lift a ∅) ⊨ τ
-  Fⁿ⊨τ zero = ⊨-anticongˡ (≤-reflexive (lift-cong a ∅)) (⊨-congʳ (≤-min τ) ∅⊨τ⊥)
-  Fⁿ⊨τ (suc n) = ⊨-mono (Fⁿ⊨τ n)
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
+  module τ₃ = Type τ₃
 
-  ^-mono : ∀ {m n} → m ≤ⁿ n → (F ^ m) (Lift a ∅) ≤ˡ (F ^ n) (Lift a ∅)
-  ^-mono {n = n} z≤n = ≤-trans (≤-reflexive (lift-cong a ∅)) (≤ˡ-min ((F ^ n) (Lift a ∅)))
-  ^-mono (s≤s m≤n) = ≤-mono (^-mono m≤n)
+∨-comm : ∀ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) → τ₁ ∨ τ₂ ≈ τ₂ ∨ τ₁
+∨-comm τ₁ τ₂ = record
+  { n≡n   = ∨ᵇ-comm τ₁.null τ₂.null
+  ; f₁⊆f₂ = [ inj₂ , inj₁ ]′
+  ; f₁⊇f₂ = [ inj₂ , inj₁ ]′
+  ; l₁⊆l₂ = [ inj₂ , inj₁ ]′
+  ; l₁⊇l₂ = [ inj₂ , inj₁ ]′
+  }
+  where
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
+
+∨-identityˡ : ∀ (τ : Type fℓ₁ lℓ₁) → τ⊥ {fℓ₂} {lℓ₂} ∨ τ ≈ τ
+∨-identityˡ τ = record
+  { n≡n   = ∨ᵇ-identityˡ null
+  ; f₁⊆f₂ = [ (λ ()) , id ]′
+  ; f₁⊇f₂ = inj₂
+  ; l₁⊆l₂ = [ (λ ()) , id ]′
+  ; l₁⊇l₂ = inj₂
+  }
+  where open Type τ
+
+∨-identityʳ : ∀ (τ : Type fℓ₁ lℓ₁) → τ ∨ τ⊥ {fℓ₂} {lℓ₂} ≈ τ
+∨-identityʳ τ = record
+  { n≡n   = ∨ᵇ-identityʳ null
+  ; f₁⊆f₂ = [ id , (λ ()) ]′
+  ; f₁⊇f₂ = inj₁
+  ; l₁⊆l₂ = [ id , (λ ()) ]′
+  ; l₁⊇l₂ = inj₁
+  }
+  where open Type τ
+
+∨-identity :
+  (∀ (τ : Type fℓ₁ lℓ₁) → τ⊥ {fℓ₂} {lℓ₂} ∨ τ ≈ τ) × (∀ (τ : Type fℓ₁ lℓ₁) → τ ∨ τ⊥ {fℓ₂} {lℓ₂} ≈ τ)
+∨-identity = ∨-identityˡ , ∨-identityʳ
+
+∙-distribʳ-∨ :
+  ∀ (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) (τ₃ : Type fℓ₃ lℓ₃) →
+  (τ₂ ∨ τ₃) ∙ τ₁ ≈ τ₂ ∙ τ₁ ∨ τ₃ ∙ τ₁
+∙-distribʳ-∨ τ₁ τ₂ τ₃ = record
+  { n≡n   = ∧-distribʳ-∨ τ₁.null τ₂.null τ₃.null
+  ; f₁⊆f₂ = [ map inj₁ inj₁ , map inj₂ inj₂ ∘ ⇒ᵗ-∨ᵇ τ₂.null τ₃.null τ₁.first ]′
+  ; f₁⊇f₂ =
+    [ [ inj₁ ∘ inj₁ , inj₂ ∘ ⇒ᵗ-∨ᵇ′ˡ τ₂.null τ₃.null τ₁.first ]′
+    , [ inj₁ ∘ inj₂ , inj₂ ∘ ⇒ᵗ-∨ᵇ′ʳ τ₂.null τ₃.null τ₁.first ]′
+    ]′
+  ; l₁⊆l₂ =
+    [ inj₁ ∘ inj₁
+    , [ inj₁ ∘ inj₂ ∘ ⇒ᵗ-monoʳ τ₁.null inj₁
+      , map (inj₂ ∘ ⇒ᵗ-monoʳ τ₁.null inj₂) (inj₂ ∘ ⇒ᵗ-monoʳ τ₁.null inj₂) ∘
+        ⇒ᵗ-⊎ τ₁.null τ₂.flast τ₃.flast
+      ]′ ∘
+      ⇒ᵗ-⊎ τ₁.null τ₁.first (λ c → τ₂.flast c ⊎ τ₃.flast c)
+    ]′
+  ; l₁⊇l₂ =
+    [ map id
+          ( [ ⇒ᵗ-monoʳ τ₁.null inj₁ , ⇒ᵗ-monoʳ τ₁.null (inj₂ ∘ inj₁) ]′ ∘
+            ⇒ᵗ-⊎ τ₁.null τ₁.first τ₂.flast
+          )
+    , map id
+          ( [ ⇒ᵗ-monoʳ τ₁.null inj₁ , ⇒ᵗ-monoʳ τ₁.null (inj₂ ∘ inj₂) ]′ ∘
+            ⇒ᵗ-⊎ τ₁.null τ₁.first τ₃.flast
+          )
+    ]′
+  }
+  where
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
+  module τ₃ = Type τ₃
+
+∨-idem : ∀ (τ : Type fℓ lℓ) → τ ∨ τ ≈ τ
+∨-idem τ = record
+  { n≡n   = ∨ᵇ-idem null
+  ; f₁⊆f₂ = reduce
+  ; f₁⊇f₂ = inj₁
+  ; l₁⊆l₂ = reduce
+  ; l₁⊇l₂ = inj₁
+  }
+  where open Type τ
+
+------------------------------------------------------------------------
+-- Structures
+
+∨-isMagma : IsMagma _≈_ (_∨_ {fℓ} {lℓ})
+∨-isMagma = record
+  { isEquivalence = ≈-isEquivalence
+  ; ∙-cong        = ∨-cong
+  }
+
+∨-isCommutativeMagma : IsCommutativeMagma _≈_ (_∨_ {fℓ} {lℓ})
+∨-isCommutativeMagma = record
+  { isMagma = ∨-isMagma
+  ; comm    = ∨-comm
+  }
+
+∨-isSemigroup : IsSemigroup _≈_ (_∨_ {fℓ} {lℓ})
+∨-isSemigroup = record
+  { isMagma = ∨-isMagma
+  ; assoc   = ∨-assoc
+  }
+
+∨-isBand : IsBand _≈_ (_∨_ {fℓ} {lℓ})
+∨-isBand = record
+  { isSemigroup = ∨-isSemigroup
+  ; idem        = ∨-idem
+  }
+
+∨-isCommutativeSemigroup : IsCommutativeSemigroup _≈_ (_∨_ {fℓ} {lℓ})
+∨-isCommutativeSemigroup = record
+  { isSemigroup = ∨-isSemigroup
+  ; comm        = ∨-comm
+  }
+
+∨-isSemilattice : IsSemilattice _≈_ (_∨_ {fℓ} {lℓ})
+∨-isSemilattice = record
+  { isBand = ∨-isBand
+  ; comm   = ∨-comm
+  }
+
+∨-isMonoid : IsMonoid _≈_ (_∨_ {fℓ} {lℓ}) τ⊥
+∨-isMonoid = record
+  { isSemigroup = ∨-isSemigroup
+  ; identity    = ∨-identity
+  }
+
+∨-isCommutativeMonoid : IsCommutativeMonoid _≈_ (_∨_ {fℓ} {lℓ}) τ⊥
+∨-isCommutativeMonoid = record
+  { isMonoid = ∨-isMonoid
+  ; comm     = ∨-comm
+  }
+
+∨-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _≈_ (_∨_ {fℓ} {lℓ}) τ⊥
+∨-isIdempotentCommutativeMonoid = record
+  { isCommutativeMonoid = ∨-isCommutativeMonoid
+  ; idem                = ∨-idem
+  }
+
+------------------------------------------------------------------------
+-- Bundles
+
+∨-magma : ∀ {fℓ} {lℓ} → Magma _ _
+∨-magma {fℓ} {lℓ} = record { isMagma = ∨-isMagma {fℓ} {lℓ} }
+
+∨-commutativeMagma : ∀ {fℓ} {lℓ} → CommutativeMagma _ _
+∨-commutativeMagma {fℓ} {lℓ} = record { isCommutativeMagma = ∨-isCommutativeMagma {fℓ} {lℓ} }
+
+∨-semigroup : ∀ {fℓ} {lℓ} → Semigroup _ _
+∨-semigroup {fℓ} {lℓ} = record { isSemigroup = ∨-isSemigroup {fℓ} {lℓ} }
+
+∨-band : ∀ {fℓ} {lℓ} → Band _ _
+∨-band {fℓ} {lℓ} = record { isBand = ∨-isBand {fℓ} {lℓ} }
+
+∨-commutativeSemigroup : ∀ {fℓ} {lℓ} → CommutativeSemigroup _ _
+∨-commutativeSemigroup {fℓ} {lℓ} = record { isCommutativeSemigroup = ∨-isCommutativeSemigroup {fℓ} {lℓ} }
+
+∨-semilattice : ∀ {fℓ} {lℓ} → Semilattice _ _
+∨-semilattice {fℓ} {lℓ} = record { isSemilattice = ∨-isSemilattice {fℓ} {lℓ} }
+
+∨-monoid : ∀ {fℓ} {lℓ} → Monoid _ _
+∨-monoid {fℓ} {lℓ} = record { isMonoid = ∨-isMonoid {fℓ} {lℓ} }
+
+∨-commutativeMonoid : ∀ {fℓ} {lℓ} → CommutativeMonoid _ _
+∨-commutativeMonoid {fℓ} {lℓ} = record { isCommutativeMonoid = ∨-isCommutativeMonoid {fℓ} {lℓ} }
+
+∨-idempotentCommutativeMonoid : ∀ {fℓ} {lℓ} → IdempotentCommutativeMonoid _ _
+∨-idempotentCommutativeMonoid {fℓ} {lℓ} = record
+  { isIdempotentCommutativeMonoid = ∨-isIdempotentCommutativeMonoid {fℓ} {lℓ} }
+
+------------------------------------------------------------------------
+-- Other properties
+
+#⇒∨-pres-⊨ : τ₁ # τ₂ → A ⊨ τ₁ → B ⊨ τ₂ → A ∪ B ⊨ τ₁ ∨ τ₂
+#⇒∨-pres-⊨ τ₁#τ₂ A⊨τ₁ B⊨τ₂ = record
+  { n⇒n = (Equivalence.from T-∨ ⟨$⟩_) ∘ map A⊨τ₁.n⇒n B⊨τ₂.n⇒n
+  ; f⇒f = map A⊨τ₁.f⇒f B⊨τ₂.f⇒f ∘ uncurry λ w → [ inj₁ ∘ (w ,_) , inj₂ ∘ (w ,_) ]′
+  ; l⇒l =
+    map A⊨τ₁.l⇒l B⊨τ₂.l⇒l ∘
+    uncurry λ _ → uncurry λ _ → uncurry
+      [ inj₁ ∘₂ (λ xw∈A → uncurry λ _ →
+        [ -,_ ∘ -,_ ∘ (xw∈A ,_) ∘ -,_
+        , ⊥-elim ∘ ∄[f₁∩f₂] ∘ (A⊨τ₁.f⇒f (-, xw∈A) ,_) ∘ B⊨τ₂.f⇒f ∘ -,_
+        ]′)
+      , inj₂ ∘₂ (λ xw∈B → uncurry λ _ →
+        [ (⊥-elim ∘ ∄[f₁∩f₂] ∘ (_, B⊨τ₂.f⇒f (-, xw∈B)) ∘ A⊨τ₁.f⇒f ∘ -,_)
+        , -,_ ∘ -,_ ∘ (xw∈B ,_) ∘ -,_
+        ]′)
+      ]′
+  }
+  where
+  open _#_ τ₁#τ₂
+  module A⊨τ₁ = _⊨_ A⊨τ₁
+  module B⊨τ₂ = _⊨_ B⊨τ₂