Clean-up Language hierarchy.

9 files changed, 1034 insertions, 605 deletions

diff --git a/src/Cfe/Function/Power.agda b/src/Cfe/Function/Power.agda
new file mode 100644
index 0000000..da3b335
--- /dev/null
+++ b/src/Cfe/Function/Power.agda
@@ -0,0 +1,37 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Cfe.Function.Power where
+
+open import Data.Nat using (ℕ)
+open import Data.Product using (∃-syntax; _×_)
+open import Function using (id; _∘_)
+open import Level using (Level; _⊔_)
+open import Relation.Binary using (Rel; REL)
+open import Relation.Binary.PropositionalEquality using (cong; _≡_)
+
+private
+  variable
+    a : Level
+    A : Set a
+
+infix 10 _^_
+
+------------------------------------------------------------------------
+-- Definition
+
+_^_ : (A → A) → ℕ → A → A
+f ^ ℕ.zero = id
+f ^ ℕ.suc n = f ∘ f ^ n
+
+------------------------------------------------------------------------
+-- Properties
+
+f∼g⇒fⁿ∼gⁿ :
+  ∀ {a b ℓ} {A : Set a} {B : Set b} (_∼_ : REL A B ℓ) {f g 0A 0B} →
+  0A ∼ 0B → (∀ {x y} → x ∼ y → f x ∼ g y) → ∀ n → (f ^ n) 0A ∼ (g ^ n) 0B
+f∼g⇒fⁿ∼gⁿ _ refl ext    ℕ.zero = refl
+f∼g⇒fⁿ∼gⁿ ∼ refl ext (ℕ.suc n) = ext (f∼g⇒fⁿ∼gⁿ ∼ refl ext n)
+
+fⁿf≡fⁿ⁺¹ : ∀ (f : A → A) n → (f ^ n) ∘ f ≡ f ^ (ℕ.suc n)
+fⁿf≡fⁿ⁺¹ f    ℕ.zero = _≡_.refl
+fⁿf≡fⁿ⁺¹ f (ℕ.suc n) = cong (f ∘_) (fⁿf≡fⁿ⁺¹ f n)
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index 71ee7df..2919ed7 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary using (REL; Setoid; _⟶_Respects_)
 
 module Cfe.Language.Base
   {c ℓ} (over : Setoid c ℓ)
@@ -8,73 +8,138 @@ module Cfe.Language.Base
 
 open Setoid over using () renaming (Carrier to C)
 
-open import Algebra
-open import Data.Empty
-open import Data.List hiding (null)
+open import Cfe.Function.Power
+open import Data.Empty.Polymorphic using (⊥)
+open import Data.List
 open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Product
-open import Data.Unit using (⊤; tt)
-open import Function hiding (_⟶_)
-open import Level as L hiding (Lift)
-open import Relation.Binary.PropositionalEquality
+open import Data.Sum
+open import Function
+open import Level
+open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Nullary using (Dec; ¬_)
 
-infix 4 _∈_
-infix 4 _∉_
-infix 4 _≈_
-infix 4 _≤_
+private
+  variable
+    a b : Level
+
+------------------------------------------------------------------------
+-- Definition
 
 record Language a : Set (c ⊔ ℓ ⊔ suc a) where
   field
-    𝕃 : List C → Set a
+    𝕃        : List C → Set a
     ∈-resp-≋ : 𝕃 ⟶ 𝕃 Respects _≋_
 
-∅ : Language 0ℓ
+------------------------------------------------------------------------
+-- Special Languages
+
+∅ : Language a
 ∅ = record
-  { 𝕃 = const ⊥
+  { 𝕃        = const ⊥
   ; ∈-resp-≋ = λ _ ()
   }
 
-｛ε｝ : Language c
-｛ε｝ = record
-  { 𝕃 = [] ≡_
-  ; ∈-resp-≋ = λ { [] refl → refl}
+｛ε｝ : Language (c ⊔ a)
+｛ε｝ {a} = record
+  { 𝕃        = Lift a ∘ ([] ≡_)
+  ; ∈-resp-≋ = λ { [] → id }
   }
 
-Lift : ∀ {a} → (b : Level) → Language a → Language (a ⊔ b)
-Lift b A = record
-  { 𝕃 = L.Lift b ∘ A.𝕃
-  ; ∈-resp-≋ = λ { eq (lift l∈A) → lift (A.∈-resp-≋ eq l∈A)}
+｛_｝ : C → Language _
+｛ c ｝ = record
+  { 𝕃        = [ c ] ≋_
+  ; ∈-resp-≋ = λ l₁≋l₂ l₁∈｛c｝ → ≋-trans l₁∈｛c｝ l₁≋l₂
   }
-  where
-  module A = Language A
 
-_∈_ : ∀ {a} → List C → Language a → Set a
+------------------------------------------------------------------------
+-- Membership
+
+infix 4 _∈_ _∉_
+
+_∈_ : List C → Language a → Set _
 _∈_ = flip Language.𝕃
 
-_∉_ : ∀ {a} → List C → Language a → Set a
-l ∉ A = l ∈ A → ⊥
+_∉_ : List C → Language a → Set _
+w ∉ A = ¬ w ∈ A
 
-record _≤_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ a ⊔ b) where
-  field
-    f : ∀ {l} → l ∈ A → l ∈ B
+------------------------------------------------------------------------
+-- Language Combinators
 
-record _≈_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔ b) where
-  field
-    f : ∀ {l} → l ∈ A → l ∈ B
-    f⁻¹ : ∀ {l} → l ∈ B → l ∈ A
+infix 7 _∙_
+infix 6 _∪_
+infix 5 ⋃_
 
-record _<_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔ b) where
-  field
-    f : ∀ {l} → l ∈ A → l ∈ B
-    l : List C
-    l∉A : l ∉ A
-    l∈B : l ∈ B
+_∙_ : Language a → Language b → Language _
+A ∙ B = record
+  { 𝕃        = λ w → ∃₂ λ w₁ w₂ → w₁ ∈ A × w₂ ∈ B × w₁ ++ w₂ ≋ w
+  ; ∈-resp-≋ = λ w≋w′ (_ , _ , w₁∈A , w₂∈B , eq) → -, -, w₁∈A , w₂∈B , ≋-trans eq w≋w′
+  }
+
+_∪_ : Language a → Language b → Language _
+A ∪ B = record
+  { 𝕃        = λ w → w ∈ A ⊎ w ∈ B
+  ; ∈-resp-≋ = uncurry Data.Sum.map ∘ < Language.∈-resp-≋ A , Language.∈-resp-≋ B >
+  }
+
+Sup : (Language a → Language a) → Language a → Language _
+Sup F A = record
+  { 𝕃        = λ w → ∃[ n ] w ∈ (F ^ n) A
+  ; ∈-resp-≋ = λ w≋w′ (n , w∈FⁿA) → n , Language.∈-resp-≋ ((F ^ n) A) w≋w′ w∈FⁿA
+  }
+
+⋃_ : (Language a → Language a) → Language _
+⋃ F = Sup F ∅
+
+------------------------------------------------------------------------
+-- Relations
+
+infix 4 _⊆_ _≈_
+
+data _⊆_ {a b} : REL (Language a) (Language b) (c ⊔ ℓ ⊔ suc (a ⊔ b)) where
+  sub : ∀ {A : Language a} {B : Language b} → (∀ {w} → w ∈ A → w ∈ B) → A ⊆ B
+
+_⊇_ : REL (Language a) (Language b) _
+_⊇_ = flip _⊆_
+
+_≈_ : REL (Language a) (Language b) _
+A ≈ B = A ⊆ B × B ⊆ A
+
+_≉_ : REL (Language a) (Language b) _
+A ≉ B = ¬ A ≈ B
+
+------------------------------------------------------------------------
+-- Membership Properties
+
+-- Contains empty string
+
+Null : ∀ {a} → Language a → Set a
+Null A = [] ∈ A
+
+-- Characters that start strings
+
+First : ∀ {a} → Language a → C → Set (c ⊔ a)
+First A c = ∃[ w ] c ∷ w ∈ A
+
+-- Characters that can follow a string to make another string in the language
+
+Flast : ∀ {a} → Language a → C → Set (c ⊔ a)
+Flast A c = ∃₂ λ c′ w → (c′ ∷ w ∈ A × ∃[ w′ ] c′ ∷ w ++ c ∷ w′ ∈ A)
+
+------------------------------------------------------------------------
+-- Proof Properties
+
+-- Membership is decidable
+
+Decidable : Language a → Set _
+Decidable A = ∀ w → Dec (w ∈ A)
+
+-- Membership proofs are irrelevant
 
-null : ∀ {a} → Language a → Set a
-null A = [] ∈ A
+Irrelevant : Language a → Set _
+Irrelevant A = ∀ {w} → (p q : w ∈ A) → p ≡ q
 
-first : ∀ {a} → Language a → C → Set (c ⊔ a)
-first A x = ∃[ l ] x ∷ l ∈ A
+-- Membership proofs are recomputable
 
-flast : ∀ {a} → Language a → C → Set (c ⊔ a)
-flast A x = ∃[ l ] (l ≢ [] × l ∈ A × ∃[ l′ ] l ++ x ∷ l′ ∈ A)
+Recomputable : Language a → Set _
+Recomputable A = ∀ {w} → .(w ∈ A) → w ∈ A
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
deleted file mode 100644
index c7baa48..0000000
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ /dev/null
@@ -1,247 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Relation.Binary
-
-module Cfe.Language.Construct.Concatenate
-  {c ℓ} (over : Setoid c ℓ)
-  where
-
-open import Algebra
-open import Cfe.Language over as 𝕃
-open import Data.Empty
-open import Data.List hiding (null)
-open import Data.List.Relation.Binary.Equality.Setoid over
-open import Data.List.Properties
-open import Data.Product as Product
-open import Data.Unit using (⊤)
-open import Function
-open import Level
-import Relation.Binary.PropositionalEquality as ≡
-open import Relation.Nullary
-open import Relation.Unary hiding (_∈_)
-import Relation.Binary.Indexed.Heterogeneous as I
-
-open Setoid over using () renaming (Carrier to C; _≈_ to _∼_; refl to ∼-refl; sym to ∼-sym; trans to ∼-trans)
-
-module Compare where
-  data Compare : List C → List C → List C → List C → Set (c ⊔ ℓ) where
-    back : ∀ {xs zs} → (xs≋zs : xs ≋ zs) → Compare [] xs [] zs
-    left : ∀ {w ws xs z zs} → Compare ws xs [] zs → (w∼z : w ∼ z) → Compare (w ∷ ws) xs [] (z ∷ zs)
-    right : ∀ {x xs y ys zs} → Compare [] xs ys zs → (x∼y : x ∼ y) → Compare [] (x ∷ xs) (y ∷ ys) zs
-    front : ∀ {w ws xs y ys zs} → Compare ws xs ys zs → (w∼y : w ∼ y) → Compare (w ∷ ws) xs (y ∷ ys) zs
-
-  isLeft : ∀ {ws xs ys zs} → Compare ws xs ys zs → Set
-  isLeft (back xs≋zs) = ⊥
-  isLeft (left cmp w∼z) = ⊤
-  isLeft (right cmp x∼y) = ⊥
-  isLeft (front cmp w∼y) = isLeft cmp
-
-  isRight : ∀ {ws xs ys zs} → Compare ws xs ys zs → Set
-  isRight (back xs≋zs) = ⊥
-  isRight (left cmp w∼z) = ⊥
-  isRight (right cmp x∼y) = ⊤
-  isRight (front cmp w∼y) = isRight cmp
-
-  isEqual : ∀ {ws xs ys zs} → Compare ws xs ys zs → Set
-  isEqual (back xs≋zs) = ⊤
-  isEqual (left cmp w∼z) = ⊥
-  isEqual (right cmp x∼y) = ⊥
-  isEqual (front cmp w∼y) = isEqual cmp
-
-  <?> : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → Tri (isLeft cmp) (isEqual cmp) (isRight cmp)
-  <?> (back xs≋zs) = tri≈ id _ id
-  <?> (left cmp w∼z) = tri< _ id id
-  <?> (right cmp x∼y) = tri> id id _
-  <?> (front cmp w∼y) = <?> cmp
-
-  compare : ∀ ws xs ys zs → ws ++ xs ≋ ys ++ zs → Compare ws xs ys zs
-  compare [] xs [] zs eq = back eq
-  compare [] (x ∷ xs) (y ∷ ys) zs (x∼y ∷ eq) = right (compare [] xs ys zs eq) x∼y
-  compare (w ∷ ws) xs [] (z ∷ zs) (w∼z ∷ eq) = left (compare ws xs [] zs eq) w∼z
-  compare (w ∷ ws) xs (y ∷ ys) zs (w∼y ∷ eq) = front (compare ws xs ys zs eq) w∼y
-
-  left-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → isLeft cmp → ∃[ w ] ∃[ ws′ ] ws ≋ ys ++ w ∷ ws′ × w ∷ ws′ ++ xs ≋ zs
-  left-split (left (back xs≋zs) w∼z) _ = -, -, ≋-refl , w∼z ∷ xs≋zs
-  left-split (left (left cmp w′∼z′) w∼z) _ with left-split (left cmp w′∼z′) _
-  ... | (_ , _ , eq₁ , eq₂) = -, -, ∼-refl ∷ eq₁ , w∼z ∷ eq₂
-  left-split (front cmp w∼y) l with left-split cmp l
-  ... | (_ , _ , eq₁ , eq₂) = -, -, w∼y ∷ eq₁ , eq₂
-
-  right-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → isRight cmp → ∃[ y ] ∃[ ys′ ] ws ++ y ∷ ys′ ≋ ys × xs ≋ y ∷ ys′ ++ zs
-  right-split (right (back xs≋zs) x∼y) _ = -, -, ≋-refl , x∼y ∷ xs≋zs
-  right-split (right (right cmp x′∼y′) x∼y) _ with right-split (right cmp x′∼y′) _
-  ... | (_ , _ , eq₁ , eq₂) = -, -, ∼-refl ∷ eq₁ , x∼y ∷ eq₂
-  right-split (front cmp w∼y) r with right-split cmp r
-  ... | (_ , _ , eq₁ , eq₂) = -, -, w∼y ∷ eq₁ , eq₂
-
-  eq-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → isEqual cmp → ws ≋ ys × xs ≋ zs
-  eq-split (back xs≋zs) e = [] , xs≋zs
-  eq-split (front cmp w∼y) e = map₁ (w∼y ∷_) (eq-split cmp e)
-
-module _
-  {a b}
-  (A : Language a)
-  (B : Language b)
-  where
-
-  private
-    module A = Language A
-    module B = Language B
-
-  infix 7 _∙_
-
-  record Concat (l : List C) : Set (c ⊔ ℓ ⊔ a ⊔ b) where
-    field
-      l₁ : List C
-      l₂ : List C
-      l₁∈A : l₁ ∈ A
-      l₂∈B : l₂ ∈ B
-      eq : l₁ ++ l₂ ≋ l
-
-  _∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b)
-  _∙_ = record
-    { 𝕃 = Concat
-    ; ∈-resp-≋ = λ
-      { l≋l′ record { l₁ = _ ; l₂ = _ ; l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = eq } → record
-        { l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = ≋-trans eq l≋l′ }
-      }
-    }
-
-∙-cong : ∀ {a} → Congruent₂ _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
-∙-cong X≈Y U≈V = record
-  { f = λ
-    { record { l₁∈A = l₁∈X ; l₂∈B = l₂∈Y ; eq = eq } → record
-      { l₁∈A = X≈Y.f l₁∈X
-      ; l₂∈B = U≈V.f l₂∈Y
-      ; eq = eq
-      }
-    }
-  ; f⁻¹ = λ
-    { record { l₁∈A = l₁∈Y ; l₂∈B = l₂∈V ; eq = eq } → record
-      { l₁∈A = X≈Y.f⁻¹ l₁∈Y
-      ; l₂∈B = U≈V.f⁻¹ l₂∈V
-      ; eq = eq
-      }
-    }
-  }
-  where
-  module X≈Y = _≈_ X≈Y
-  module U≈V = _≈_ U≈V
-
-∙-assoc : ∀ {a b c} (A : Language a) (B : Language b) (C : Language c) →
-          (A ∙ B) ∙ C ≈ A ∙ (B ∙ C)
-∙-assoc A B C = record
-  { f = λ
-    { record
-      { l₂ = l₃
-      ; l₁∈A = record { l₁ = l₁ ; l₂ = l₂ ; l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = eq₁ }
-      ; l₂∈B = l₃∈C
-      ; eq = eq₂
-      } → record
-      { l₁∈A = l₁∈A
-      ; l₂∈B = record
-        { l₁∈A = l₂∈B
-        ; l₂∈B = l₃∈C
-        ; eq = ≋-refl
-        }
-      ; eq = ≋-trans (≋-sym (≋-reflexive (++-assoc l₁ l₂ l₃))) (≋-trans (++⁺ eq₁ ≋-refl) eq₂)
-      }
-    }
-  ; f⁻¹ = λ
-    { record
-      { l₁ = l₁
-      ; l₁∈A = l₁∈A
-      ; l₂∈B = record { l₁ = l₂ ; l₂ = l₃ ; l₁∈A = l₂∈B ; l₂∈B = l₃∈C ; eq = eq₁ }
-      ; eq = eq₂
-      } → record
-      { l₁∈A = record
-        { l₁∈A = l₁∈A
-        ; l₂∈B = l₂∈B
-        ; eq = ≋-refl
-        }
-      ; l₂∈B = l₃∈C
-      ; eq = ≋-trans (≋-reflexive (++-assoc l₁ l₂ l₃)) (≋-trans (++⁺ ≋-refl eq₁) eq₂)
-      }
-    }
-  }
-
-∙-identityˡ : ∀ {a} → LeftIdentity _≈_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝) _∙_
-∙-identityˡ X = record
-  { f = λ
-    { record { l₁ = [] ; l₂∈B = l∈X ; eq = eq } → X.∈-resp-≋ eq l∈X
-    }
-  ; f⁻¹ = λ l∈X → record
-    { l₁∈A = lift ≡.refl
-    ; l₂∈B = l∈X
-    ; eq = ≋-refl
-    }
-  }
-  where
-  module X = Language X
-
-∙-identityʳ : ∀ {a} → RightIdentity _≈_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝) _∙_
-∙-identityʳ X = record
-  { f = λ
-    { record { l₁ = l₁ ; l₂ = [] ; l₁∈A = l∈X ; eq = eq } → X.∈-resp-≋ (≋-trans (≋-sym (≋-reflexive (++-identityʳ l₁))) eq) l∈X
-    }
-  ; f⁻¹ = λ {l} l∈X → record
-    { l₁∈A = l∈X
-    ; l₂∈B = lift ≡.refl
-    ; eq = ≋-reflexive (++-identityʳ l)
-    }
-  }
-  where
-  module X = Language X
-
-∙-mono : ∀ {a b} → _∙_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
-∙-mono X≤Y U≤V = record
-  { f = λ
-    { record { l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = eq } → record
-      { l₁∈A = X≤Y.f l₁∈A
-      ; l₂∈B = U≤V.f l₂∈B
-      ; eq = eq
-      }
-    }
-  }
-  where
-  module X≤Y = _≤_ X≤Y
-  module U≤V = _≤_ U≤V
-
-∙-unique : ∀ {a b} (A : Language a) (B : Language b) → Empty (flast A ∩ first B) → ¬ (null A) → ∀ {l} → (l∈A∙B l∈A∙B′ : l ∈ A ∙ B) → Concat.l₁ l∈A∙B ≋ Concat.l₁ l∈A∙B′ × Concat.l₂ l∈A∙B ≋ Concat.l₂ l∈A∙B′
-∙-unique A B ∄[l₁∩f₂] ¬n₁ l∈A∙B l∈A∙B′ with Compare.compare (Concat.l₁ l∈A∙B) (Concat.l₂ l∈A∙B) (Concat.l₁ l∈A∙B′) (Concat.l₂ l∈A∙B′) (≋-trans (Concat.eq l∈A∙B) (≋-sym (Concat.eq l∈A∙B′)))
-... | cmp with Compare.<?> cmp
-... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] w ((-, (λ { ≡.refl → ¬n₁ (Concat.l₁∈A l∈A∙B′)}) , (Concat.l₁∈A l∈A∙B′) , -, A.∈-resp-≋ eq₃ (Concat.l₁∈A l∈A∙B)) , (-, B.∈-resp-≋ (≋-sym eq₄) (Concat.l₂∈B l∈A∙B′))))
-  where
-  module A = Language A
-  module B = Language B
-  lsplit = Compare.left-split cmp l
-  w = proj₁ lsplit
-  eq₃ = (proj₁ ∘ proj₂ ∘ proj₂) lsplit
-  eq₄ = (proj₂ ∘ proj₂ ∘ proj₂) lsplit
-... | tri≈ _ e _ = Compare.eq-split cmp e
-... | tri> _ _ r = ⊥-elim (∄[l₁∩f₂] w ((-, (λ { ≡.refl → ¬n₁ (Concat.l₁∈A l∈A∙B)}) , (Concat.l₁∈A l∈A∙B) , -, A.∈-resp-≋ (≋-sym eq₃) (Concat.l₁∈A l∈A∙B′)) , (-, (B.∈-resp-≋ eq₄ (Concat.l₂∈B l∈A∙B)))))
-  where
-  module A = Language A
-  module B = Language B
-  rsplit = Compare.right-split cmp r
-  w = proj₁ rsplit
-  eq₃ = (proj₁ ∘ proj₂ ∘ proj₂) rsplit
-  eq₄ = (proj₂ ∘ proj₂ ∘ proj₂) rsplit
-
-isMagma : ∀ {a} → IsMagma _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
-isMagma {a} = record
-  { isEquivalence = ≈-isEquivalence
-  ; ∙-cong = ∙-cong {a}
-  }
-
-isSemigroup : ∀ {a} → IsSemigroup _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
-isSemigroup {a} = record
-  { isMagma = isMagma {a}
-  ; assoc = ∙-assoc
-  }
-
-isMonoid : ∀ {a} → IsMonoid _≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝)
-isMonoid {a} = record
-  { isSemigroup = isSemigroup {a}
-  ; identity = ∙-identityˡ {a} , ∙-identityʳ {a}
-  }
diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda
deleted file mode 100644
index ddea1a6..0000000
--- a/src/Cfe/Language/Construct/Single.agda
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Function
-open import Relation.Binary
-import Relation.Binary.PropositionalEquality as ≡
-
-module Cfe.Language.Construct.Single
-  {c ℓ} (over : Setoid c ℓ)
-  where
-
-open Setoid over renaming (Carrier to C)
-
-open import Cfe.Language over hiding (_≈_)
-open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid over
-open import Data.Product as Product
-open import Data.Unit
-open import Level
-
-｛_｝ : C → Language (c ⊔ ℓ)
-｛ c ｝ = record
-  { 𝕃 = [ c ] ≋_
-  ; ∈-resp-≋ = λ l₁≋l₂ l₁∈｛c｝ → ≋-trans l₁∈｛c｝ l₁≋l₂
-  }
-
-xy∉｛c｝ : ∀ c x y l → x ∷ y ∷ l ∉ ｛ c ｝
-xy∉｛c｝ c x y l (_ ∷ ())
diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda
deleted file mode 100644
index 0865123..0000000
--- a/src/Cfe/Language/Construct/Union.agda
+++ /dev/null
@@ -1,84 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Relation.Binary
-
-module Cfe.Language.Construct.Union
-  {c ℓ} (over : Setoid c ℓ)
-  where
-
-open import Algebra
-open import Data.Empty
-open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid over
-open import Data.Product as Product
-open import Data.Sum as Sum
-open import Function
-open import Level
-open import Cfe.Language over as 𝕃 hiding (Lift)
-
-open Setoid over renaming (Carrier to C)
-
-module _
-  {a b}
-  (A : Language a)
-  (B : Language b)
-  where
-
-  private
-    module A = Language A
-    module B = Language B
-
-  infix 6 _∪_
-
-  Union : List C → Set (a ⊔ b)
-  Union l = l ∈ A ⊎ l ∈ B
-
-  _∪_ : Language (a ⊔ b)
-  _∪_ = record
-    { 𝕃 = Union
-    ; ∈-resp-≋ = λ l₁≋l₂ → Sum.map (A.∈-resp-≋ l₁≋l₂) (B.∈-resp-≋ l₁≋l₂)
-    }
-
-isCommutativeMonoid : ∀ {a} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a ∅)
-isCommutativeMonoid = record
-  { isMonoid = record
-    { isSemigroup = record
-      { isMagma = record
-        { isEquivalence = ≈-isEquivalence
-        ; ∙-cong = λ X≈Y U≈V → record
-          { f = Sum.map (_≈_.f X≈Y) (_≈_.f U≈V)
-          ; f⁻¹ = Sum.map (_≈_.f⁻¹ X≈Y) (_≈_.f⁻¹ U≈V)
-          }
-        }
-      ; assoc = λ A B C → record
-        { f = Sum.assocʳ
-        ; f⁻¹ = Sum.assocˡ
-        }
-      }
-    ; identity = (λ A → record
-      { f = λ { (inj₂ x) → x }
-      ; f⁻¹ = inj₂
-      }) , (λ A → record
-      { f = λ { (inj₁ x) → x }
-      ; f⁻¹ = inj₁
-      })
-    }
-  ; comm = λ A B → record
-    { f = Sum.swap
-    ; f⁻¹ = Sum.swap
-    }
-  }
-
-∪-mono : ∀ {a b} → _∪_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
-∪-mono X≤Y U≤V = record
-  { f = Sum.map X≤Y.f U≤V.f
-  }
-  where
-  module X≤Y = _≤_ X≤Y
-  module U≤V = _≤_ U≤V
-
-∪-unique : ∀ {a b} {A : Language a} {B : Language b} → (∀ x → first A x → first B x → ⊥) → (𝕃.null A → 𝕃.null B → ⊥) → ∀ {l} → l ∈ A ∪ B → (l ∈ A × l ∉ B) ⊎ (l ∉ A × l ∈ B)
-∪-unique fA∩fB≡∅ ¬nA∨¬nB {[]}    (inj₁ []∈A) = inj₁ ([]∈A , ¬nA∨¬nB []∈A)
-∪-unique fA∩fB≡∅ ¬nA∨¬nB {x ∷ l} (inj₁ xl∈A) = inj₁ (xl∈A , (λ xl∈B → fA∩fB≡∅ x (-, xl∈A) (-, xl∈B)))
-∪-unique fA∩fB≡∅ ¬nA∨¬nB {[]}    (inj₂ []∈B) = inj₂ (flip ¬nA∨¬nB []∈B , []∈B)
-∪-unique fA∩fB≡∅ ¬nA∨¬nB {x ∷ l} (inj₂ xl∈B) = inj₂ ((λ xl∈A → fA∩fB≡∅ x (-, xl∈A) (-, xl∈B)) , xl∈B)
diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
deleted file mode 100644
index 0ae9100..0000000
--- a/src/Cfe/Language/Indexed/Construct/Iterate.agda
+++ /dev/null
@@ -1,88 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Relation.Binary as B using (Setoid)
-
-module Cfe.Language.Indexed.Construct.Iterate
-  {c ℓ} (over : Setoid c ℓ)
-  where
-
-open Setoid over using () renaming (Carrier to C)
-
-open import Algebra
-open import Cfe.Language over as L
-open import Cfe.Language.Indexed.Homogeneous over
-open import Data.List
-open import Data.Nat as ℕ hiding (_⊔_; _≤_; _^_)
-open import Data.Product as Product
-open import Function
-open import Level hiding (Lift) renaming (suc to lsuc)
-open import Relation.Binary.Indexed.Heterogeneous
-open import Relation.Binary.PropositionalEquality as ≡
-
-open IndexedLanguage
-
-infix 9 _^_
-
-_^_ : ∀ {a} {A : Set a} → Op₁ A → ℕ → Op₁ A
-f ^ zero = id
-f ^ (suc n) = f ∘ (f ^ n)
-
-f-fn-x≡fn-f-x : ∀ {a} {A : Set a} (f : A → A) n x → f ((f ^ n) x) ≡ (f ^ n) (f x)
-f-fn-x≡fn-f-x f ℕ.zero x = refl
-f-fn-x≡fn-f-x f (suc n) x = ≡.cong f (f-fn-x≡fn-f-x f n x)
-
-module _
-  {a aℓ} (A : B.Setoid a aℓ)
-  where
-
-  private
-    module A = B.Setoid A
-
-  f≈g⇒fn≈gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≈ y → f x A.≈ g y) → ∀ n x → (f ^ n) x A.≈ (g ^ n) x
-  f≈g⇒fn≈gn f≈g ℕ.zero x = A.refl
-  f≈g⇒fn≈gn f≈g (suc n) x = f≈g (f≈g⇒fn≈gn f≈g n x)
-
-module _
-  {a aℓ₁ aℓ₂} (A : B.Poset a aℓ₁ aℓ₂)
-  where
-
-  private
-    module A = B.Poset A
-
-  f≤g⇒fn≤gn : {f g : A.Carrier → A.Carrier} → (∀ {x y} → x A.≤ y → f x A.≤ g y) → ∀ n x → (f ^ n) x A.≤ (g ^ n) x
-  f≤g⇒fn≤gn f≤g ℕ.zero x = A.refl
-  f≤g⇒fn≤gn f≤g (suc n) x = f≤g (f≤g⇒fn≤gn f≤g n x)
-
-module _
-  {a}
-  where
-  Iterate : (Language a → Language a) → IndexedLanguage 0ℓ 0ℓ a
-  Iterate f = record
-    { Carrierᵢ = ℕ
-    ; _≈ᵢ_ = ≡._≡_
-    ; isEquivalenceᵢ = ≡.isEquivalence
-    ; F = λ n → (f ^ n) (Lift a ∅)
-    ; cong = λ {≡.refl → ≈-refl}
-    }
-
-  ⋃ : (Language a → Language a) → Language a
-  ⋃ f = record
-    { 𝕃 = Iter.Tagged
-    ; ∈-resp-≋ = λ { l₁≋l₂ (i , l₁∈fi) → i , Language.∈-resp-≋ (Iter.F i) l₁≋l₂ l₁∈fi }
-    }
-    where
-    module Iter = IndexedLanguage (Iterate f)
-
-  fⁿ≤⋃f : ∀ f n → (f ^ n) (Lift a ∅) ≤ ⋃ f
-  fⁿ≤⋃f f n = record { f = n ,_ }
-
-  ⋃-cong : ∀ {f g} → (∀ {x y} → x ≈ y → f x ≈ g y) → ⋃ f ≈ ⋃ g
-  ⋃-cong f≈g = record
-    { f = λ { (n , l∈fn) → n , _≈_.f (f≈g⇒fn≈gn (L.setoid a) f≈g n (Lift a ∅)) l∈fn}
-    ; f⁻¹ = λ { (n , l∈gn) → n , _≈_.f⁻¹ (f≈g⇒fn≈gn (L.setoid a) f≈g n (Lift a ∅)) l∈gn}
-    }
-
-  ⋃-mono : ∀ {f g} → (∀ {x y} → x ≤ y → f x ≤ g y) → ⋃ f ≤ ⋃ g
-  ⋃-mono f≤g = record
-    { f = λ { (n , l∈fn) → n , _≤_.f (f≤g⇒fn≤gn (poset a) f≤g n (Lift a ∅)) l∈fn }
-    }
diff --git a/src/Cfe/Language/Indexed/Homogeneous.agda b/src/Cfe/Language/Indexed/Homogeneous.agda
deleted file mode 100644
index 44e3b6c..0000000
--- a/src/Cfe/Language/Indexed/Homogeneous.agda
+++ /dev/null
@@ -1,30 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Relation.Binary as B using (Setoid)
-
-module Cfe.Language.Indexed.Homogeneous
-  {c ℓ} (over : Setoid c ℓ)
-  where
-
-open import Cfe.Language over
-open import Level
-open import Data.List
-open import Data.Product
-open import Relation.Binary.Indexed.Heterogeneous
-
-open _≈_
-
-open Setoid over using () renaming (Carrier to C)
-
-record IndexedLanguage i iℓ a : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a)) where
-  field
-    Carrierᵢ : Set i
-    _≈ᵢ_ : B.Rel Carrierᵢ iℓ
-    isEquivalenceᵢ : B.IsEquivalence _≈ᵢ_
-    F : Carrierᵢ → Language a
-    cong : F B.Preserves _≈ᵢ_ ⟶ _≈_
-
-  open B.IsEquivalence isEquivalenceᵢ using () renaming (refl to reflᵢ; sym to symᵢ; trans to transᵢ) public
-
-  Tagged : List C → Set (i ⊔ a)
-  Tagged l = ∃[ i ] l ∈ F i
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index 52b5470..5792216 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -1,123 +1,815 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary hiding (Decidable; Irrelevant; Recomputable)
 
 module Cfe.Language.Properties
   {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid over using () renaming (Carrier to C)
+open Setoid over using () renaming (Carrier to C; _≈_ to _∼_; refl to ∼-refl)
+
+open import Algebra
+open import Cfe.Function.Power
 open import Cfe.Language.Base over
-open import Data.List
+open import Cfe.List.Compare over
+open import Data.Empty using (⊥-elim)
+import Data.Fin as Fin
+open import Data.List as L
+open import Data.List.Properties
 open import Data.List.Relation.Binary.Equality.Setoid over
-open import Function
-open import Level hiding (Lift)
+import Data.List.Relation.Unary.Any as Any
+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)
+import Relation.Binary.Construct.On as On
+open import Relation.Binary.PropositionalEquality hiding (setoid; [_])
+open import Relation.Nullary hiding (Irrelevant)
+open import Relation.Nullary.Decidable
+open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Nullary.Sum using (_⊎-dec_)
 
-≈-refl : ∀ {a} → Reflexive (_≈_ {a})
-≈-refl {x = A} = record
-  { f = id
-  ; f⁻¹ = id
-  }
+private
+  variable
+    a b d ℓ₁ ℓ₂ : Level
+    A X : Language b
+    B Y : Language d
+    U Z : Language ℓ₁
+    V : Language ℓ₂
+    F : Language a → Language a
+    G : Language b → Language b
 
-≈-sym : ∀ {a b} → Sym (_≈_ {a} {b}) _≈_
-≈-sym A≈B = record
-  { f = A≈B.f⁻¹
-  ; f⁻¹ = A≈B.f
-  }
-  where
-  module A≈B = _≈_ A≈B
+  w++[]≋w : ∀ w → w ++ [] ≋ w
+  w++[]≋w [] = []
+  w++[]≋w (x ∷ w) = ∼-refl ∷ w++[]≋w w
+
+------------------------------------------------------------------------
+-- Properties of _⊆_
+------------------------------------------------------------------------
+-- Relational properties of _⊆_
+
+⊆-refl : Reflexive (_⊆_ {a})
+⊆-refl = sub id
+
+⊆-reflexive : (_≈_ {a} {b}) ⇒ _⊆_
+⊆-reflexive = proj₁
+
+⊇-reflexive : (_≈_ {a} {b}) ⇒ flip _⊆_
+⊇-reflexive = proj₂
+
+⊆-trans : Trans (_⊆_ {a}) (_⊆_ {b} {d}) _⊆_
+⊆-trans (sub A⊆B) (sub B⊆C) = sub (B⊆C ∘ A⊆B)
+
+⊆-antisym : Antisym (_⊆_ {a} {b}) _⊆_ _≈_
+⊆-antisym = _,_
+
+------------------------------------------------------------------------
+-- Membership properties of _⊆_
+
+∈-resp-⊆ : ∀ {w} → (w ∈_) ⟶ (w ∈_) Respects (_⊆_ {a} {b})
+∈-resp-⊆ (sub A⊆B) = A⊆B
 
-≈-trans : ∀ {a b c} → Trans (_≈_ {a}) (_≈_ {b} {c}) _≈_
-≈-trans {i = A} {B} {C} A≈B B≈C = record
-  { f = B≈C.f ∘ A≈B.f
-  ; f⁻¹ = A≈B.f⁻¹ ∘ B≈C.f⁻¹
+∉-resp-⊇ : ∀ {w} → (w ∉_) ⟶ (w ∉_) Respects flip (_⊆_ {b} {a})
+∉-resp-⊇ (sub A⊇B) w∉A = w∉A ∘ A⊇B
+
+Null-resp-⊆ : Null {a} ⟶ Null {b} Respects _⊆_
+Null-resp-⊆ = ∈-resp-⊆
+
+First-resp-⊆ : ∀ {c} → flip (First {a}) c ⟶ flip (First {a}) 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-⊆ (sub A⊆B) = P.map₂ (P.map₂ (P.map A⊆B (P.map₂ A⊆B)))
+
+------------------------------------------------------------------------
+-- Properties of _≈_
+------------------------------------------------------------------------
+-- Relational properties of _≈_
+
+≈-refl : Reflexive (_≈_ {a})
+≈-refl = ⊆-refl , ⊆-refl
+
+≈-sym : Sym (_≈_ {a} {b}) _≈_
+≈-sym = P.swap
+
+≈-trans : Trans (_≈_ {a}) (_≈_ {b} {d}) _≈_
+≈-trans = P.zip ⊆-trans (flip ⊆-trans)
+
+------------------------------------------------------------------------
+-- Structures
+
+≈-isPartialEquivalence : IsPartialEquivalence (_≈_ {a})
+≈-isPartialEquivalence = record
+  { sym = ≈-sym
+  ; trans = ≈-trans
   }
-  where
-  module A≈B = _≈_ A≈B
-  module B≈C = _≈_ B≈C
 
-≈-isEquivalence : ∀ {a} → IsEquivalence (_≈_ {a})
+≈-isEquivalence : IsEquivalence (_≈_ {a})
 ≈-isEquivalence = record
   { refl = ≈-refl
   ; sym = ≈-sym
   ; trans = ≈-trans
   }
 
-setoid : ∀ a → Setoid (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a)
-setoid a = record { isEquivalence = ≈-isEquivalence {a} }
-
-≤-refl : ∀ {a} → Reflexive (_≤_ {a})
-≤-refl = record
-  { f = id
+⊆-isPreorder : IsPreorder (_≈_ {a}) _⊆_
+⊆-isPreorder = record
+  { isEquivalence = ≈-isEquivalence
+  ; reflexive = ⊆-reflexive
+  ; trans = ⊆-trans
   }
 
-≤-reflexive : ∀ {a b} → _≈_ {a} {b} ⇒ _≤_
-≤-reflexive A≈B = record
-  { f = A≈B.f
+⊆-isPartialOrder : IsPartialOrder (_≈_ {a}) _⊆_
+⊆-isPartialOrder = record
+  { isPreorder = ⊆-isPreorder
+  ; antisym = ⊆-antisym
   }
+
+------------------------------------------------------------------------
+-- Bundles
+
+partialSetoid : PartialSetoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+partialSetoid {a} = record { isPartialEquivalence = ≈-isPartialEquivalence {a} }
+
+setoid : Setoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+setoid {a} = record { isEquivalence = ≈-isEquivalence {a} }
+
+⊆-preorder : Preorder (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+⊆-preorder {a} = record { isPreorder = ⊆-isPreorder {a} }
+
+⊆-poset : Poset (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+⊆-poset {a} = record { isPartialOrder = ⊆-isPartialOrder {a} }
+
+------------------------------------------------------------------------
+-- Membership properties of _≈_
+
+∈-resp-≈ : ∀ {w} → (w ∈_) ⟶ (w ∈_) Respects (_≈_ {a} {b})
+∈-resp-≈ = ∈-resp-⊆ ∘ ⊆-reflexive
+
+∉-resp-≈ : ∀ {w} → (w ∉_) ⟶ (w ∉_) Respects flip (_≈_ {b} {a})
+∉-resp-≈ = ∉-resp-⊇ ∘ ⊆-reflexive
+
+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-≈ = First-resp-⊆ ∘ ⊆-reflexive
+
+Flast-resp-≈ : ∀ {c} → flip (Flast {a}) c ⟶ flip (Flast {a}) c Respects _≈_
+Flast-resp-≈ = Flast-resp-⊆ ∘ ⊆-reflexive
+
+------------------------------------------------------------------------
+-- Proof properties of _≈_
+
+Decidable-resp-≈ : Decidable {a} ⟶ Decidable {b} Respects _≈_
+Decidable-resp-≈ (sub A⊆B , sub A⊇B) A? l = map′ A⊆B A⊇B (A? l)
+
+Recomputable-resp-≈ : Recomputable {a} ⟶ Recomputable {b} Respects _≈_
+Recomputable-resp-≈ (sub A⊆B , sub A⊇B) recomp l∈B = A⊆B (recomp (A⊇B l∈B))
+
+------------------------------------------------------------------------
+-- Properties of ∅
+------------------------------------------------------------------------
+-- Algebraic properties of ∅
+
+⊆-min : Min (_⊆_ {a} {b}) ∅
+⊆-min _ = sub λ ()
+
+------------------------------------------------------------------------
+-- Membership properties of ∅
+
+w∉∅ : ∀ w → w ∉ ∅ {a}
+w∉∅ _ ()
+
+ε∉∅ : ¬ Null {a} ∅
+ε∉∅ ()
+
+∄[First[∅]] : ∀ c → ¬ First {a} ∅ c
+∄[First[∅]] _ ()
+
+∄[Flast[∅]] : ∀ c → ¬ Flast {a} ∅ c
+∄[Flast[∅]] _ ()
+
+ε∉A+∄[First[A]]⇒A≈∅ : ¬ Null A → (∀ c → ¬ First A c) → A ≈ ∅ {a}
+ε∉A+∄[First[A]]⇒A≈∅ {A = A} ε∉A cw∉A =
+  ⊆-antisym
+    (sub λ {w} w∈A → case ∃[ w ] w ∈ A ∋ w , w∈A of λ
+      { ([]    ,  ε∈A) → lift (ε∉A ε∈A)
+      ; (c ∷ w , cw∈A) → lift (cw∉A c (w , cw∈A))
+      })
+    (⊆-min A)
+
+------------------------------------------------------------------------
+-- Proof properties of ∅
+
+∅? : Decidable (∅ {a})
+∅? w = no λ ()
+
+∅-irrelevant : Irrelevant (∅ {a})
+∅-irrelevant ()
+
+∅-recomputable : Recomputable (∅ {a})
+∅-recomputable ()
+
+------------------------------------------------------------------------
+-- Properties of ｛ε｝
+------------------------------------------------------------------------
+-- Membership properties of ∅
+
+ε∈｛ε｝ : Null (｛ε｝{a})
+ε∈｛ε｝ = lift refl
+
+∄[First[｛ε｝]] : ∀ c → ¬ First (｛ε｝ {a}) c
+∄[First[｛ε｝]] _ ()
+
+∄[Flast[｛ε｝]] : ∀ c → ¬ Flast (｛ε｝ {a}) c
+∄[Flast[｛ε｝]] _ ()
+
+∄[First[A]]⇒A⊆｛ε｝ : (∀ c → ¬ First A c) → A ⊆ ｛ε｝ {a}
+∄[First[A]]⇒A⊆｛ε｝ {A = A} cw∉A =
+  sub λ {w} w∈A → case ∃[ w ] w ∈ A ∋ w , w∈A return (λ (w , _) → w ∈ ｛ε｝) of λ
+    { ([]    ,  w∈A) → lift refl
+    ; (c ∷ w , cw∈A) → ⊥-elim (cw∉A c (w , cw∈A))
+    }
+
+------------------------------------------------------------------------
+-- Proof properties of ｛ε｝
+
+｛ε｝? : Decidable (｛ε｝ {a})
+｛ε｝? []      = yes (lift refl)
+｛ε｝? (_ ∷ _) = no λ ()
+
+｛ε｝-irrelevant : Irrelevant (｛ε｝ {a})
+｛ε｝-irrelevant (lift refl) (lift refl) = refl
+
+｛ε｝-recomputable : Recomputable (｛ε｝ {a})
+｛ε｝-recomputable {w = []} _ = lift refl
+
+------------------------------------------------------------------------
+-- Properties of ｛_｝
+------------------------------------------------------------------------
+-- Membership properties of ｛_｝
+
+ε∉｛c｝ : ∀ c → ¬ Null ｛ c ｝
+ε∉｛c｝ _ ()
+
+c′∈First[｛c｝]⇒c∼c′ : ∀ {c c′} → First ｛ c ｝ c′ → c ∼ c′
+c′∈First[｛c｝]⇒c∼c′ (_ , c∼c′ ∷ []) = c∼c′
+
+c∼c′⇒c′∈｛c｝ : ∀ {c c′} → c ∼ c′ → [ c′ ] ∈ ｛ c ｝
+c∼c′⇒c′∈｛c｝ c∼c′ = c∼c′ ∷ []
+
+∄[Flast[｛c｝]] : ∀ {c} c′ → ¬ Flast ｛ c ｝ c′
+∄[Flast[｛c｝]] _ (_ , _ , _ ∷ [] , _ , _ ∷ ())
+
+xyw∉｛c｝ : ∀ c x y w → x ∷ y ∷ w ∉ ｛ c ｝
+xyw∉｛c｝ c x y w (_ ∷ ())
+
+------------------------------------------------------------------------
+-- Properties of _∙_
+------------------------------------------------------------------------
+-- Membership properties of _∙_
+
+-- Null
+
+ε∈A⇒B⊆A∙B : ∀ (A : Language b) (B : Language d) → Null A → B ⊆ A ∙ B
+ε∈A⇒B⊆A∙B _ _ ε∈A = sub λ w∈B → -, -, ε∈A , w∈B , ≋-refl
+
+ε∈B⇒A⊆A∙B : ∀ (A : Language b) (B : Language d) → Null B → A ⊆ A ∙ B
+ε∈B⇒A⊆A∙B _ _ ε∈B = sub λ {w} w∈A → -, -, w∈A , ε∈B , w++[]≋w w
+
+ε∈A+ε∈B⇒ε∈A∙B : Null A → Null B → Null (A ∙ B)
+ε∈A+ε∈B⇒ε∈A∙B ε∈A ε∈B = -, -, ε∈A , ε∈B , ≋-refl
+
+ε∈A∙B⇒ε∈A : ∀ (A : Language b) (B : Language d) → Null (A ∙ B) → Null A
+ε∈A∙B⇒ε∈A _ _ ([] , [] , ε∈A , ε∈B , []) = ε∈A
+
+ε∈A∙B⇒ε∈B : ∀ (A : Language b) (B : Language d) → Null (A ∙ B) → Null B
+ε∈A∙B⇒ε∈B _ _ ([] , [] , ε∈A , ε∈B , []) = ε∈B
+
+-- First
+
+c∈First[A]+w′∈B⇒c∈First[A∙B] : ∀ {c} → First A c → ∃[ w ] w ∈ B → First (A ∙ B) c
+c∈First[A]+w′∈B⇒c∈First[A∙B] (_ , cw∈A) (_ , w′∈B) = -, -, -, cw∈A , w′∈B , ≋-refl
+
+ε∈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
+
+-- Flast
+
+c∈Flast[B]+w∈A⇒c∈Flast[A∙B] : ∀ {c} → Flast B c → ∃[ w ] w ∈ A → Flast (A ∙ B) c
+c∈Flast[B]+w∈A⇒c∈Flast[A∙B]         (_ , _ ,  w∈B , _ ,  wcw′∈B) (       [] ,     ε∈A) =
+  -, -, (-, -, ε∈A , w∈B , ≋-refl) , -, -, -, ε∈A , wcw′∈B , ≋-refl
+c∈Flast[B]+w∈A⇒c∈Flast[A∙B] {c = c} (x , w , xw∈B , w′ , xwcw′∈B) (c′ ∷ w′′ , c′w′′∈A) =
+  -, -, c′w′′xw∈A∙B , -, c′w′′xwcw′∈A∙B
   where
-  module A≈B = _≈_ A≈B
+  c′w′′xw∈A∙B    = -, -, c′w′′∈A , xw∈B , ≋-refl
+  c′w′′xwcw′∈A∙B = -, -, c′w′′∈A , xwcw′∈B , ∼-refl ∷ ≋-reflexive (sym (++-assoc w′′ (x ∷ w) (c ∷ w′)))
 
-≤-trans : ∀ {a b c} → Trans (_≤_ {a}) (_≤_ {b} {c}) _≤_
-≤-trans A≤B B≤C = record
-  { f = B≤C.f ∘ A≤B.f
-  }
+ε∈B+x∈First[A]+c∈First[B]⇒c∈Flast[A∙B] :
+  ∀ {c} → Null B → ∃[ x ] First A x → First B c → Flast (A ∙ B) c
+ε∈B+x∈First[A]+c∈First[B]⇒c∈Flast[A∙B] ε∈B (x , w , xw∈A) (_ , cw′∈B) = -, -, xw∈A∙B , -, xwcw′∈A∙B
   where
-  module A≤B = _≤_ A≤B
-  module B≤C = _≤_ B≤C
+  xw∈A∙B    = -, -, xw∈A , ε∈B , w++[]≋w (x ∷ w)
+  xwcw′∈A∙B = -, -, xw∈A , cw′∈B , ≋-refl
 
-≤-antisym : ∀ {a b} → Antisym (_≤_ {a} {b}) _≤_ _≈_
-≤-antisym A≤B B≤A = record
-  { f = A≤B.f
-  ; f⁻¹ = B≤A.f
-  }
+ε∈B+c∈Flast[A]⇒c∈Flast[A∙B] : ∀ {c} → Null B → Flast A c → Flast (A ∙ B) c
+ε∈B+c∈Flast[A]⇒c∈Flast[A∙B] {c = c} ε∈B (x , w , xw∈A , w′ , xwcw′∈A) = -, -, xw∈A∙B , -, xwcw′∈A∙B
   where
-  module A≤B = _≤_ A≤B
-  module B≤A = _≤_ B≤A
+  xw∈A∙B    = -, -, xw∈A , ε∈B , w++[]≋w (x ∷ w)
+  xwcw′∈A∙B = -, -, xwcw′∈A , ε∈B , w++[]≋w (x ∷ w ++ c ∷ w′)
 
-≤-min : ∀ {b} → Min (_≤_ {b = b}) ∅
-≤-min A = record
-  { f = λ ()
-  }
+------------------------------------------------------------------------
+-- Algebraic properties of _∙_
 
-≤-isPartialOrder : ∀ a → IsPartialOrder (_≈_ {a}) _≤_
-≤-isPartialOrder a = record
-  { isPreorder = record
-    { isEquivalence = ≈-isEquivalence
-    ; reflexive = ≤-reflexive
-    ; trans = ≤-trans
-    }
-  ; antisym = ≤-antisym
+∙-mono : X ⊆ Y → U ⊆ V → X ∙ U ⊆ Y ∙ V
+∙-mono (sub X⊆Y) (sub U⊆V) = sub λ (_ , _ , w₁∈X , w₂∈U , eq) → -, -, X⊆Y w₁∈X , U⊆V w₂∈U , eq
+
+∙-cong : X ≈ Y → U ≈ V → X ∙ U ≈ Y ∙ V
+∙-cong X≈Y U≈V = ⊆-antisym
+  (∙-mono (⊆-reflexive X≈Y) (⊆-reflexive U≈V))
+  (∙-mono (⊇-reflexive X≈Y) (⊇-reflexive U≈V))
+
+∙-assoc : ∀ (A : Language a) (B : Language b) (C : Language d) → (A ∙ B) ∙ C ≈ A ∙ (B ∙ C)
+∙-assoc A B C =
+  (sub λ {w} (w₁w₂ , w₃ , (w₁ , w₂ , w₁∈A , w₂∈B , eq₁) , w₃∈C , eq₂) →
+    -, -, w₁∈A , (-, -, w₂∈B , w₃∈C , ≋-refl) ,
+      (begin
+        w₁ ++ w₂ ++ w₃   ≡˘⟨ ++-assoc w₁ w₂ w₃ ⟩
+        (w₁ ++ w₂) ++ w₃ ≈⟨ ++⁺ eq₁ ≋-refl ⟩
+        w₁w₂ ++ w₃       ≈⟨ eq₂ ⟩
+        w ∎)) ,
+  (sub λ {w} (w₁ , w₂w₃ , w₁∈A , (w₂ , w₃ , w₂∈B , w₃∈C , eq₁) , eq₂) →
+    -, -, (-, -, w₁∈A , w₂∈B , ≋-refl) , w₃∈C ,
+      (begin
+        (w₁ ++ w₂) ++ w₃ ≡⟨ ++-assoc w₁ w₂ w₃ ⟩
+        w₁ ++ w₂ ++ w₃   ≈⟨ ++⁺ ≋-refl eq₁ ⟩
+        w₁ ++ w₂w₃       ≈⟨ eq₂ ⟩
+        w ∎))
+  where
+  open import Relation.Binary.Reasoning.Setoid ≋-setoid
+
+∙-identityˡ : ∀ (A : Language a) → ｛ε｝ {b} ∙ A ≈ A
+∙-identityˡ A =
+  ⊆-antisym
+    (sub λ { (_ , _ , lift refl , w′∈A , eq) → A.∈-resp-≋ eq w′∈A })
+    (ε∈A⇒B⊆A∙B ｛ε｝ A ε∈｛ε｝)
+  where
+  module A = Language A
+
+∙-identityʳ : ∀ (A : Language a) → A ∙ ｛ε｝ {b} ≈ A
+∙-identityʳ X =
+  ⊆-antisym
+    (sub λ {w} → λ
+      { (w′ , _ , w′∈X , lift refl , eq) →
+        X.∈-resp-≋
+          (begin
+            w′       ≈˘⟨ w++[]≋w w′ ⟩
+            w′ ++ [] ≈⟨ eq ⟩
+            w        ∎)
+          w′∈X
+      })
+    (ε∈B⇒A⊆A∙B X ｛ε｝ ε∈｛ε｝)
+  where
+  open import Relation.Binary.Reasoning.Setoid ≋-setoid
+  module X = Language X
+
+∙-identity : (∀ (A : Language a) → ｛ε｝ {b} ∙ A ≈ A) × (∀ (A : Language a) → A ∙ ｛ε｝ {b} ≈ A)
+∙-identity = ∙-identityˡ , ∙-identityʳ
+
+∙-zeroˡ : ∀ (A : Language a) → ∅ {b} ∙ A ≈ ∅ {d}
+∙-zeroˡ A = ⊆-antisym (sub λ ()) (⊆-min (∅ ∙ A))
+
+∙-zeroʳ : ∀ (A : Language a) → A ∙ ∅ {b} ≈ ∅ {d}
+∙-zeroʳ A = ⊆-antisym (sub λ ()) (⊆-min (A ∙ ∅))
+
+∙-zero : (∀ (A : Language a) → ∅ {b} ∙ A ≈ ∅ {d}) × (∀ (A : Language a) → A ∙ ∅ {b} ≈ ∅ {d})
+∙-zero = ∙-zeroˡ , ∙-zeroʳ
+
+-- Structures
+
+∙-isMagma : ∀ {a} → IsMagma _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
+∙-isMagma = record
+  { isEquivalence = ≈-isEquivalence
+  ; ∙-cong        = ∙-cong
   }
 
-poset : ∀ a → Poset (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) (c ⊔ a)
-poset a = record { isPartialOrder = ≤-isPartialOrder a }
+∙-isSemigroup : ∀ {a} → IsSemigroup _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
+∙-isSemigroup {a} = record
+  { isMagma = ∙-isMagma {a}
+  ; assoc   = ∙-assoc
+  }
 
-<-trans : ∀ {a b c} → Trans (_<_ {a}) (_<_ {b} {c}) _<_
-<-trans A<B B<C = record
-  { f = B<C.f ∘ A<B.f
-  ; l = A<B.l
-  ; l∉A = A<B.l∉A
-  ; l∈B = B<C.f A<B.l∈B
+∙-isMonoid : ∀ {a} → IsMonoid _≈_ _∙_ (｛ε｝ {ℓ ⊔ a})
+∙-isMonoid {a} = record
+  { isSemigroup = ∙-isSemigroup {a}
+  ; identity    = ∙-identity
   }
+
+-- Bundles
+
+∙-Magma : ∀ {a} → Magma (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∙-Magma {a} = record { isMagma = ∙-isMagma {a} }
+
+∙-Semigroup : ∀ {a} → Semigroup (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∙-Semigroup {a} = record { isSemigroup = ∙-isSemigroup {a} }
+
+∙-Monoid : ∀ {a} → Monoid (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∙-Monoid {a} = record { isMonoid = ∙-isMonoid {a} }
+
+------------------------------------------------------------------------
+-- Other properties of _∙_
+
+∙-uniqueₗ :
+  ∀ (A : Language a) (B : Language b) →
+  (∀ {c} → ¬ (Flast A c × First B c)) →
+  ¬ Null A →
+  ∀ {w} (p q : w ∈ A ∙ B) → (_≋_ on proj₁) p q
+∙-uniqueₗ A B ∄[l₁∩f₂] ε∉A (   [] , _ , ε∈A , _             )                  _                       = ⊥-elim (ε∉A ε∈A)
+∙-uniqueₗ A B ∄[l₁∩f₂] ε∉A (_ ∷ _  , _                      ) ([] , _ , ε∈A , _                      ) = ⊥-elim (ε∉A ε∈A)
+∙-uniqueₗ A B ∄[l₁∩f₂] ε∉A (x ∷ w₁ , w₂ , xw₁∈A , w₂∈B , eq₁) (x′ ∷ w₁′ , w₂′ , x′w₁′∈A , w₂′∈B , eq₂)
+  with compare (x ∷ w₁) w₂ (x′ ∷ w₁′) w₂′ (≋-trans eq₁ (≋-sym eq₂))
+... | cmp with <?> cmp
+... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] (c∈Flast[A] , c∈First[B]))
+  where
+  module A   = Language A
+  module B   = Language B
+  lsplit     = left-split cmp l
+  xw∈A       = x′w₁′∈A
+  xwcw′∈A    = A.∈-resp-≋ ((proj₁ ∘ proj₂ ∘ proj₂) lsplit) xw₁∈A
+  cw′∈B      = B.∈-resp-≋ (≋-sym ((proj₂ ∘ proj₂ ∘ proj₂) lsplit)) w₂′∈B
+  c∈Flast[A] = -, -, xw∈A , -, xwcw′∈A
+  c∈First[B] = -, cw′∈B
+... | tri≈ _ e _ = proj₁ (eq-split cmp e)
+... | tri> _ _ r = ⊥-elim (∄[l₁∩f₂] (c∈Flast[A] , c∈First[B]))
   where
-  module A<B = _<_ A<B
-  module B<C = _<_ B<C
+  module A   = Language A
+  module B   = Language B
+  rsplit     = right-split cmp r
+  xw∈A       = xw₁∈A
+  xwcw′∈A    = A.∈-resp-≋ (≋-sym ((proj₁ ∘ proj₂ ∘ proj₂) rsplit)) x′w₁′∈A
+  cw′∈B      = B.∈-resp-≋ ((proj₂ ∘ proj₂ ∘ proj₂) rsplit) w₂∈B
+  c∈Flast[A] = -, -, xw∈A , -, xwcw′∈A
+  c∈First[B] = -, cw′∈B
 
-<-irrefl : ∀ {a b} → Irreflexive (_≈_ {a} {b}) _<_
-<-irrefl A≈B A<B = A<B.l∉A (A≈B.f⁻¹ A<B.l∈B)
+∙-uniqueᵣ :
+  ∀ (A : Language a) (B : Language b) →
+  (∀ {c} → ¬ (Flast A c × First B c)) →
+  ¬ Null A →
+  ∀ {w} (p q : w ∈ A ∙ B) → (_≋_ on proj₁ ∘ proj₂) p q
+∙-uniqueᵣ A B ∄[l₁∩f₂] ε∉A (   []  ,  _ ,   ε∈A , _         )                                        _ = ⊥-elim (ε∉A ε∈A)
+∙-uniqueᵣ A B ∄[l₁∩f₂] ε∉A (_ ∷  _ , _                      ) (      [] ,   _ ,     ε∈A , _          ) = ⊥-elim (ε∉A ε∈A)
+∙-uniqueᵣ A B ∄[l₁∩f₂] ε∉A (x ∷ w₁ , w₂ , xw₁∈A , w₂∈B , eq₁) (x′ ∷ w₁′ , w₂′ , x′w₁′∈A , w₂′∈B , eq₂)
+  with compare (x ∷ w₁) w₂ (x′ ∷ w₁′) w₂′ (≋-trans eq₁ (≋-sym eq₂))
+... | cmp with <?> cmp
+... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] (c∈Flast[A] , c∈First[B]))
+  where
+  module A   = Language A
+  module B   = Language B
+  lsplit     = left-split cmp l
+  xw∈A       = x′w₁′∈A
+  xwcw′∈A    = A.∈-resp-≋ ((proj₁ ∘ proj₂ ∘ proj₂) lsplit) xw₁∈A
+  cw′∈B      = B.∈-resp-≋ (≋-sym ((proj₂ ∘ proj₂ ∘ proj₂) lsplit)) w₂′∈B
+  c∈Flast[A] = -, -, xw∈A , -, xwcw′∈A
+  c∈First[B] = -, cw′∈B
+... | tri≈ _ e _ = proj₂ (eq-split cmp e)
+... | tri> _ _ r = ⊥-elim (∄[l₁∩f₂] (c∈Flast[A] , c∈First[B]))
   where
-  module A≈B = _≈_ A≈B
-  module A<B = _<_ A<B
+  module A   = Language A
+  module B   = Language B
+  rsplit     = right-split cmp r
+  xw∈A       = xw₁∈A
+  xwcw′∈A    = A.∈-resp-≋ (≋-sym ((proj₁ ∘ proj₂ ∘ proj₂) rsplit)) x′w₁′∈A
+  cw′∈B      = B.∈-resp-≋ ((proj₂ ∘ proj₂ ∘ proj₂) rsplit) w₂∈B
+  c∈Flast[A] = -, -, xw∈A , -, xwcw′∈A
+  c∈First[B] = -, cw′∈B
 
-<-asym : ∀ {a} → Asymmetric (_<_ {a})
-<-asym A<B B<A = A<B.l∉A (B<A.f A<B.l∈B)
+------------------------------------------------------------------------
+-- Proof properties of _∙_
+
+_∙?_ : Decidable A → Decidable B → Decidable (A ∙ B)
+_∙?_ {A = A} {B = B} A? B? [] =
+  map′
+    (λ (ε∈A , ε∈B) → -, -, ε∈A , ε∈B , [])
+    (λ {([] , [] , ε∈A , ε∈B , []) → ε∈A , ε∈B})
+    (A? [] ×-dec B? [])
+_∙?_ {A = A} {B = B} A? B? (x ∷ w) =
+  map′
+    (λ
+      { (inj₁ (ε∈A , xw∈B))                → -, -, ε∈A , xw∈B , ≋-refl
+      ; (inj₂ (_ , _ , xw₁∈A , w₂∈B , eq)) → -, -, xw₁∈A , w₂∈B , ∼-refl ∷ eq
+      })
+    (λ
+      { (    [] , _ ,    ε∈A , w′∈B ,        eq) → inj₁ (ε∈A , B.∈-resp-≋ eq w′∈B)
+      ; (x′ ∷ _ , _ , x′w₁∈A , w₂∈B , x′∼x ∷ eq) →
+        inj₂ (-, -, A.∈-resp-≋ (x′∼x ∷ ≋-refl) x′w₁∈A , w₂∈B , eq)
+      })
+    (A? [] ×-dec B? (x ∷ w) ⊎-dec (_∙?_ {A = A′} {B = B} (A? ∘ (x ∷_)) B?) w)
   where
-  module A<B = _<_ A<B
-  module B<A = _<_ B<A
+  module A = Language A
+  module B = Language B
+  A′ : Language _
+  A′ = record
+    { 𝕃 = λ w → x ∷ w ∈ A
+    ; ∈-resp-≋ = λ w≋w′ → A.∈-resp-≋ (∼-refl ∷ w≋w′)
+    }
+
+------------------------------------------------------------------------
+-- Properties of _∪_
+------------------------------------------------------------------------
+-- Membership properties of _∪_
+
+-- Null
+
+ε∈A⇒ε∈A∪B : ∀ (A : Language b) (B : Language d) → Null A → Null (A ∪ B)
+ε∈A⇒ε∈A∪B _ _ = inj₁
+
+ε∈B⇒ε∈A∪B : ∀ (A : Language b) (B : Language d) → Null B → Null (A ∪ B)
+ε∈B⇒ε∈A∪B _ _ = inj₂
+
+ε∈A∪B⇒ε∈A⊎ε∈B : ∀ (A : Language b) (B : Language d) → Null (A ∪ B) → Null A ⊎ Null B
+ε∈A∪B⇒ε∈A⊎ε∈B _ _ = id
+
+-- First
+
+c∈First[A]⇒c∈First[A∪B] : ∀ {c} → First A c → First (A ∪ B) c
+c∈First[A]⇒c∈First[A∪B] = P.map₂ inj₁
+
+c∈First[B]⇒c∈First[A∪B] : ∀ {c} → First B c → First (A ∪ B) c
+c∈First[B]⇒c∈First[A∪B] = P.map₂ inj₂
+
+c∈First[A∪B]⇒c∈First[A]∪c∈First[B] : ∀ {c} → First (A ∪ B) c → First A c ⊎ First B c
+c∈First[A∪B]⇒c∈First[A]∪c∈First[B] (_ , cw∈A∪B) = S.map -,_ -,_ cw∈A∪B
+
+-- Flast
+
+c∈Flast[A]⇒c∈Flast[A∪B] : ∀ {c} → Flast A c → Flast (A ∪ B) c
+c∈Flast[A]⇒c∈Flast[A∪B] = P.map₂ (P.map₂ (P.map inj₁ (P.map₂ inj₁)))
+
+c∈Flast[B]⇒c∈Flast[A∪B] : ∀ {c} → Flast B c → Flast (A ∪ B) c
+c∈Flast[B]⇒c∈Flast[A∪B] = P.map₂ (P.map₂ (P.map inj₂ (P.map₂ inj₂)))
+
+-- TODO: rename this
+∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] :
+  ∀ {c} → (∀ {x} → ¬ (First A x × First B x)) → Flast (A ∪ B) c → Flast A c ⊎ Flast B c
+∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] ∄[f₁∩f₂] (_ , _ , inj₁ xw∈A , _ , inj₁ xwcw′∈A) = inj₁ (-, -, xw∈A , -, xwcw′∈A)
+∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] ∄[f₁∩f₂] (_ , _ , inj₁ xw∈A , _ , inj₂ xwcw′∈B) = ⊥-elim (∄[f₁∩f₂] ((-, xw∈A) , (-, xwcw′∈B)))
+∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] ∄[f₁∩f₂] (_ , _ , inj₂ xw∈B , _ , inj₁ xwcw′∈A) = ⊥-elim (∄[f₁∩f₂] ((-, xwcw′∈A) , (-, xw∈B)))
+∄[c∈First[A]∩First[B]]+c∈Flast[A∪B]⇒c∈Flast[A]⊎c∈Flast[B] ∄[f₁∩f₂] (_ , _ , inj₂ xw∈B , _ , inj₂ xwcw′∈B) = inj₂ (-, -, xw∈B , -, xwcw′∈B)
+
+------------------------------------------------------------------------
+-- Algebraic properties of _∪_
+
+∪-mono : X ⊆ Y → U ⊆ V → X ∪ U ⊆ Y ∪ V
+∪-mono (sub X⊆Y) (sub U⊆V) = sub (S.map X⊆Y U⊆V)
+
+∪-cong : X ≈ Y → U ≈ V → X ∪ U ≈ Y ∪ V
+∪-cong X≈Y U≈V = ⊆-antisym
+  (∪-mono (⊆-reflexive X≈Y) (⊆-reflexive U≈V))
+  (∪-mono (⊇-reflexive X≈Y) (⊇-reflexive U≈V))
+
+∪-assoc : ∀ (A : Language a) (B : Language b) (C : Language d) → (A ∪ B) ∪ C ≈ A ∪ (B ∪ C)
+∪-assoc _ _ _ = ⊆-antisym (sub S.assocʳ) (sub S.assocˡ)
+
+∪-comm : ∀ (A : Language a) (B : Language b) → A ∪ B ≈ B ∪ A
+∪-comm _ _ = ⊆-antisym (sub S.swap) (sub S.swap)
+
+∪-identityˡ : ∀ (A : Language a) → ∅ {b} ∪ A ≈ A
+∪-identityˡ _ = ⊆-antisym (sub λ { (inj₁ ()) ; (inj₂ w∈A) → w∈A }) (sub inj₂)
+
+∪-identityʳ : ∀ (A : Language a) → A ∪ ∅ {b} ≈ A
+∪-identityʳ _ = ⊆-antisym (sub λ { (inj₁ w∈A) → w∈A ; (inj₂ ()) }) (sub inj₁)
+
+∪-identity : (∀ (A : Language a) → ∅ {b} ∪ A ≈ A) × (∀ (A : Language a) → A ∪ ∅ {b} ≈ A)
+∪-identity = ∪-identityˡ , ∪-identityʳ
+
+∙-distribˡ-∪ : ∀ (A : Language a) (B : Language b) (C : Language d) → A ∙ (B ∪ C) ≈ A ∙ B ∪ A ∙ C
+∙-distribˡ-∪ _ _ _ =
+  ⊆-antisym
+    (sub λ
+      { (_ , _ , w₁∈A , inj₁ w₂∈B , eq) → inj₁ (-, -, w₁∈A , w₂∈B , eq)
+      ; (_ , _ , w₁∈A , inj₂ w₂∈C , eq) → inj₂ (-, -, w₁∈A , w₂∈C , eq)
+      })
+    (sub λ
+      { (inj₁ (_ , _ , w₁∈A , w₂∈B , eq)) → -, -, w₁∈A , inj₁ w₂∈B , eq
+      ; (inj₂ (_ , _ , w₁∈A , w₂∈C , eq)) → -, -, w₁∈A , inj₂ w₂∈C , eq
+      })
+
+∙-distribʳ-∪ : ∀ (A : Language a) (B : Language b) (C : Language d) → (B ∪ C) ∙ A ≈ B ∙ A ∪ C ∙ A
+∙-distribʳ-∪ _ _ _ =
+  ⊆-antisym
+    (sub λ
+      { (_ , _ , inj₁ w₁∈B , w₂∈A , eq) → inj₁ (-, -, w₁∈B , w₂∈A , eq)
+      ; (_ , _ , inj₂ w₁∈C , w₂∈A , eq) → inj₂ (-, -, w₁∈C , w₂∈A , eq)
+      })
+    (sub λ
+      { (inj₁ (_ , _ , w₁∈B , w₂∈A , eq)) → -, -, inj₁ w₁∈B , w₂∈A , eq
+      ; (inj₂ (_ , _ , w₁∈C , w₂∈A , eq)) → -, -, inj₂ w₁∈C , w₂∈A , eq
+      })
+
+∙-distrib-∪ :
+  (∀ (A : Language a) (B : Language b) (C : Language d) → A ∙ (B ∪ C) ≈ A ∙ B ∪ A ∙ C) ×
+  (∀ (A : Language a) (B : Language b) (C : Language d) → (B ∪ C) ∙ A ≈ B ∙ A ∪ C ∙ A)
+∙-distrib-∪ = ∙-distribˡ-∪ , ∙-distribʳ-∪
+
+∪-idem : ∀ (A : Language a) → A ∪ A ≈ A
+∪-idem A = ⊆-antisym (sub [ id , id ]′) (sub inj₁)
+
+-- Structures
+
+∪-isMagma : IsMagma _≈_ (_∪_ {a})
+∪-isMagma = record
+  { isEquivalence = ≈-isEquivalence
+  ; ∙-cong        = ∪-cong
+  }
+
+∪-isCommutativeMagma : IsCommutativeMagma _≈_ (_∪_ {a})
+∪-isCommutativeMagma = record
+  { isMagma = ∪-isMagma
+  ; comm    = ∪-comm
+  }
+
+∪-isSemigroup : IsSemigroup _≈_ (_∪_ {a})
+∪-isSemigroup = record
+  { isMagma = ∪-isMagma
+  ; assoc   = ∪-assoc
+  }
+
+∪-isBand : IsBand _≈_ (_∪_ {a})
+∪-isBand = record
+  { isSemigroup = ∪-isSemigroup
+  ; idem        = ∪-idem
+  }
+
+∪-isCommutativeSemigroup : IsCommutativeSemigroup _≈_ (_∪_ {a})
+∪-isCommutativeSemigroup = record
+  { isSemigroup = ∪-isSemigroup
+  ; comm        = ∪-comm
+  }
 
-lift-cong : ∀ {a} b (L : Language a) → Lift b L ≈ L
-lift-cong b L = record
-  { f = lower
-  ; f⁻¹ = lift
+∪-isSemilattice : IsSemilattice _≈_ (_∪_ {a})
+∪-isSemilattice = record
+  { isBand = ∪-isBand
+  ; comm   = ∪-comm
   }
+
+∪-isMonoid : IsMonoid _≈_ _∪_ (∅ {a})
+∪-isMonoid = record
+  { isSemigroup = ∪-isSemigroup
+  ; identity    = ∪-identity
+  }
+
+∪-isCommutativeMonoid : IsCommutativeMonoid _≈_ _∪_ (∅ {a})
+∪-isCommutativeMonoid = record
+  { isMonoid = ∪-isMonoid
+  ; comm     = ∪-comm
+  }
+
+∪-isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid _≈_ _∪_ (∅ {a})
+∪-isIdempotentCommutativeMonoid = record
+  { isCommutativeMonoid = ∪-isCommutativeMonoid
+  ; idem                = ∪-idem
+  }
+
+∪-∙-isNearSemiring : IsNearSemiring _≈_ _∪_ _∙_ (∅ {c ⊔ ℓ ⊔ a})
+∪-∙-isNearSemiring {a} = record
+  { +-isMonoid    = ∪-isMonoid
+  ; *-isSemigroup = ∙-isSemigroup {a}
+  ; distribʳ      = ∙-distribʳ-∪
+  ; zeroˡ         = ∙-zeroˡ
+  }
+
+∪-∙-isSemiringWithoutOne : IsSemiringWithoutOne _≈_ _∪_ _∙_ (∅ {c ⊔ ℓ ⊔ a})
+∪-∙-isSemiringWithoutOne {a} = record
+  { +-isCommutativeMonoid = ∪-isCommutativeMonoid
+  ; *-isSemigroup         = ∙-isSemigroup {a}
+  ; distrib               = ∙-distrib-∪
+  ; zero                  = ∙-zero
+  }
+
+∪-∙-isSemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _≈_ _∪_ _∙_ ∅ (｛ε｝ {ℓ ⊔ a})
+∪-∙-isSemiringWithoutAnnihilatingZero {a} = record
+  { +-isCommutativeMonoid = ∪-isCommutativeMonoid
+  ; *-isMonoid            = ∙-isMonoid {a}
+  ; distrib               = ∙-distrib-∪
+  }
+
+∪-∙-isSemiring : IsSemiring _≈_ _∪_ _∙_ ∅ (｛ε｝ {ℓ ⊔ a})
+∪-∙-isSemiring {a} = record
+  { isSemiringWithoutAnnihilatingZero = ∪-∙-isSemiringWithoutAnnihilatingZero {a}
+  ; zero                              = ∙-zero
+  }
+
+-- Bundles
+
+∪-magma : Magma (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-magma {a} = record { isMagma = ∪-isMagma {a} }
+
+∪-commutativeMagma : CommutativeMagma (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-commutativeMagma {a} = record { isCommutativeMagma = ∪-isCommutativeMagma {a} }
+
+∪-semigroup : Semigroup (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-semigroup {a} = record { isSemigroup = ∪-isSemigroup {a} }
+
+∪-band : Band (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-band {a} = record { isBand = ∪-isBand {a} }
+
+∪-commutativeSemigroup : CommutativeSemigroup (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-commutativeSemigroup {a} = record { isCommutativeSemigroup = ∪-isCommutativeSemigroup {a} }
+
+∪-semilattice : Semilattice (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-semilattice {a} = record { isSemilattice = ∪-isSemilattice {a} }
+
+∪-monoid : Monoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-monoid {a} = record { isMonoid = ∪-isMonoid {a} }
+
+∪-commutativeMonoid : CommutativeMonoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-commutativeMonoid {a} = record { isCommutativeMonoid = ∪-isCommutativeMonoid {a} }
+
+∪-idempotentCommutativeMonoid : IdempotentCommutativeMonoid (c ⊔ ℓ ⊔ lsuc a) (c ⊔ ℓ ⊔ lsuc a)
+∪-idempotentCommutativeMonoid {a} = record
+  { isIdempotentCommutativeMonoid = ∪-isIdempotentCommutativeMonoid {a} }
+
+∪-∙-nearSemiring : NearSemiring (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∪-∙-nearSemiring {a} = record { isNearSemiring = ∪-∙-isNearSemiring {a} }
+
+∪-∙-semiringWithoutOne : SemiringWithoutOne (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∪-∙-semiringWithoutOne {a} = record { isSemiringWithoutOne = ∪-∙-isSemiringWithoutOne {a} }
+
+∪-∙-semiringWithoutAnnihilatingZero : SemiringWithoutAnnihilatingZero (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∪-∙-semiringWithoutAnnihilatingZero {a} = record { isSemiringWithoutAnnihilatingZero = ∪-∙-isSemiringWithoutAnnihilatingZero {a} }
+
+∪-∙-semiring : Semiring (lsuc (c ⊔ ℓ ⊔ a)) (lsuc (c ⊔ ℓ ⊔ a))
+∪-∙-semiring {a} = record { isSemiring = ∪-∙-isSemiring {a} }
+
+------------------------------------------------------------------------
+-- Other properties of _∪_
+
+∪-selective :
+  ¬ (Null A × Null B) →
+  (∀ {c} → ¬ (First A c × First B c)) →
+  ∀ {w} → w ∈ A ∪ B → (w ∈ A × w ∉ B) ⊎ (w ∉ A × w ∈ B)
+∪-selective ε∉A∩B ∄[f₁∩f₂] {[]}    (inj₁ ε∈A) = inj₁ (ε∈A , ε∉A∩B ∘ (ε∈A ,_))
+∪-selective ε∉A∩B ∄[f₁∩f₂] {c ∷ w} (inj₁ cw∈A) = inj₁ (cw∈A , ∄[f₁∩f₂] ∘ ((w , cw∈A) ,_) ∘ (w ,_))
+∪-selective ε∉A∩B ∄[f₁∩f₂] {[]}    (inj₂ ε∈B) = inj₂ (ε∉A∩B ∘ (_, ε∈B) , ε∈B)
+∪-selective ε∉A∩B ∄[f₁∩f₂] {c ∷ w} (inj₂ cw∈B) = inj₂ (∄[f₁∩f₂] ∘ (_, (w , cw∈B)) ∘ (w ,_) , cw∈B)
+
+------------------------------------------------------------------------
+-- Proof properties of _∪_
+
+_∪?_ : Decidable A → Decidable B → Decidable (A ∪ B)
+(A? ∪? B?) w = A? w ⊎-dec B? w
+
+------------------------------------------------------------------------
+-- Properties of Sup
+------------------------------------------------------------------------
+-- Membership properties of Sup
+
+FⁿA⊆SupFA : ∀ n → (F ^ n) A ⊆ Sup F A
+FⁿA⊆SupFA n = sub (n ,_)
+
+FⁿFA⊆SupFA : ∀ n → (F ^ n) (F A) ⊆ Sup F A
+FⁿFA⊆SupFA {F = F} {A = A} n = ⊆-trans (sub (go n)) (FⁿA⊆SupFA (ℕ.suc n))
+  where
+  go : ∀ {w} n → w ∈ (F ^ n) (F A) → w ∈ (F ^ (ℕ.suc n)) A
+  go {w = w} n w∈Fⁿ̂FA = subst (λ x → w ∈ x A) (fⁿf≡fⁿ⁺¹ F n) w∈Fⁿ̂FA
+
+∀[FⁿA⊆B]⇒SupFA⊆B : (∀ n → (F ^ n) A ⊆ B) → Sup F A ⊆ B
+∀[FⁿA⊆B]⇒SupFA⊆B FⁿA⊆B = sub λ (n , w∈FⁿA) → ∈-resp-⊆ (FⁿA⊆B n) w∈FⁿA
+
+∃[B⊆FⁿA]⇒B⊆SupFA : ∀ n → B ⊆ (F ^ n) A → B ⊆ Sup F A
+∃[B⊆FⁿA]⇒B⊆SupFA n B⊆FⁿA = sub λ w∈B → n , ∈-resp-⊆ B⊆FⁿA w∈B
+
+∀[FⁿA≈GⁿB]⇒SupFA≈SupGB : (∀ n → (F ^ n) A ≈ (G ^ n) B) → Sup F A ≈ Sup G B
+∀[FⁿA≈GⁿB]⇒SupFA≈SupGB FⁿA≈GⁿB =
+  ⊆-antisym
+    (sub λ (n , w∈FⁿA) → n , ∈-resp-≈ (FⁿA≈GⁿB n) w∈FⁿA)
+    (sub λ (n , w∈GⁿB) → n , ∈-resp-≈ (≈-sym (FⁿA≈GⁿB n)) w∈GⁿB)
+------------------------------------------------------------------------
+-- Properties of ⋃_
+------------------------------------------------------------------------
+-- Membership properties of ⋃_
+
+Fⁿ⊆⋃F : ∀ n → (F ^ n) ∅ ⊆ ⋃ F
+Fⁿ⊆⋃F = FⁿA⊆SupFA
+
+∀[Fⁿ⊆B]⇒⋃F⊆B : (∀ n → (F ^ n) ∅ ⊆ B) → ⋃ F ⊆ B
+∀[Fⁿ⊆B]⇒⋃F⊆B = ∀[FⁿA⊆B]⇒SupFA⊆B
+
+∃[B⊆Fⁿ]⇒B⊆⋃F : ∀ n → B ⊆ (F ^ n) ∅ → B ⊆ ⋃ F
+∃[B⊆Fⁿ]⇒B⊆⋃F = ∃[B⊆FⁿA]⇒B⊆SupFA
+
+∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G : (∀ n → (F ^ n) ∅ ≈ (G ^ n) ∅) → ⋃ F ≈ ⋃ G
+∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G = ∀[FⁿA≈GⁿB]⇒SupFA≈SupGB
+
+------------------------------------------------------------------------
+-- Functional properties of ⋃_
+
+⋃-mono : (∀ {A B} → A ⊆ B → F A ⊆ G B) → ⋃ F ⊆ ⋃ G
+⋃-mono mono-ext = ∀[Fⁿ⊆B]⇒⋃F⊆B λ n → ⊆-trans (f∼g⇒fⁿ∼gⁿ _⊆_ (⊆-min ∅) mono-ext n) (Fⁿ⊆⋃F n)
+
+⋃-cong : (∀ {A B} → A ≈ B → F A ≈ G B) → ⋃ F ≈ ⋃ G
+⋃-cong ext = ∀[Fⁿ≈Gⁿ]⇒⋃F≈⋃G (f∼g⇒fⁿ∼gⁿ _≈_ (⊆-antisym (⊆-min ∅) (⊆-min ∅)) ext)
+
+⋃-inverseʳ : ∀ (A : Language a) → ⋃ (const A) ≈ A
+⋃-inverseʳ _ = ⊆-antisym (sub λ {(ℕ.suc _ , w∈A) → w∈A}) (Fⁿ⊆⋃F 1)
diff --git a/src/Cfe/List/Compare.agda b/src/Cfe/List/Compare.agda
new file mode 100644
index 0000000..03fbcc1
--- /dev/null
+++ b/src/Cfe/List/Compare.agda
@@ -0,0 +1,111 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Cfe.List.Compare
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+open Setoid over renaming (Carrier to C)
+
+open import Data.Empty
+open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid over
+open import Data.Product
+open import Data.Unit using (⊤)
+open import Function
+open import Level
+
+------------------------------------------------------------------------
+-- Definition
+
+data Compare : List C → List C → List C → List C → Set (c ⊔ ℓ) where
+  back : ∀ {xs zs} → (xs≋zs : xs ≋ zs) → Compare [] xs [] zs
+  left :
+    ∀ {w ws xs z zs} →
+    Compare ws xs [] zs → (w∼z : w ≈ z) →
+    Compare (w ∷ ws) xs [] (z ∷ zs)
+  right :
+    ∀ {x xs y ys zs} →
+    Compare [] xs ys zs → (x∼y : x ≈ y) →
+    Compare [] (x ∷ xs) (y ∷ ys) zs
+  front :
+    ∀ {w ws xs y ys zs} →
+    Compare ws xs ys zs →
+    (w∼y : w ≈ y) →
+    Compare (w ∷ ws) xs (y ∷ ys) zs
+
+------------------------------------------------------------------------
+-- Predicates
+
+IsLeft : ∀ {ws xs ys zs} → Compare ws xs ys zs → Set
+IsLeft (back xs≋zs)    = ⊥
+IsLeft (left cmp w∼z)  = ⊤
+IsLeft (right cmp x∼y) = ⊥
+IsLeft (front cmp w∼y) = IsLeft cmp
+
+IsRight : ∀ {ws xs ys zs} → Compare ws xs ys zs → Set
+IsRight (back xs≋zs)    = ⊥
+IsRight (left cmp w∼z)  = ⊥
+IsRight (right cmp x∼y) = ⊤
+IsRight (front cmp w∼y) = IsRight cmp
+
+IsEqual : ∀ {ws xs ys zs} → Compare ws xs ys zs → Set
+IsEqual (back xs≋zs)    = ⊤
+IsEqual (left cmp w∼z)  = ⊥
+IsEqual (right cmp x∼y) = ⊥
+IsEqual (front cmp w∼y) = IsEqual cmp
+
+-- Predicates are disjoint
+
+<?> : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → Tri (IsLeft cmp) (IsEqual cmp) (IsRight cmp)
+<?> (back xs≋zs)    = tri≈ id  _ id
+<?> (left cmp w∼z)  = tri<  _ id id
+<?> (right cmp x∼y) = tri> id id  _
+<?> (front cmp w∼y) = <?> cmp
+
+------------------------------------------------------------------------
+-- Introduction
+
+-- Construct from the equality of two pairs of lists
+
+compare : ∀ ws xs ys zs → ws ++ xs ≋ ys ++ zs → Compare ws xs ys zs
+compare []       xs       []       zs       eq         = back eq
+compare []       (x ∷ xs) (y ∷ ys) zs       (x∼y ∷ eq) = right (compare [] xs ys zs eq) x∼y
+compare (w ∷ ws) xs       []       (z ∷ zs) (w∼z ∷ eq) = left (compare ws xs [] zs eq) w∼z
+compare (w ∷ ws) xs       (y ∷ ys) zs       (w∼y ∷ eq) = front (compare ws xs ys zs eq) w∼y
+
+------------------------------------------------------------------------
+-- Elimination
+
+-- Eliminate left splits
+
+left-split :
+  ∀ {ws xs ys zs} →
+  (cmp : Compare ws xs ys zs) →
+  IsLeft cmp →
+  ∃₂ λ w ws′ → ws ≋ ys ++ w ∷ ws′ × w ∷ ws′ ++ xs ≋ zs
+left-split (left (back xs≋zs) w∼z) _ = -, -, ≋-refl , w∼z ∷ xs≋zs
+left-split (left (left cmp w′∼z′) w∼z) _ with left-split (left cmp w′∼z′) _
+... | (_ , _ , eq₁ , eq₂) = -, -, refl ∷ eq₁ , w∼z ∷ eq₂
+left-split (front cmp w∼y) l with left-split cmp l
+... | (_ , _ , eq₁ , eq₂) = -, -, w∼y ∷ eq₁ , eq₂
+
+-- Eliminate right splits
+
+right-split :
+  ∀ {ws xs ys zs} →
+  (cmp : Compare ws xs ys zs) →
+  IsRight cmp →
+  ∃₂ λ y ys′ → ws ++ y ∷ ys′ ≋ ys × xs ≋ y ∷ ys′ ++ zs
+right-split (right (back xs≋zs) x∼y) _ = -, -, ≋-refl , x∼y ∷ xs≋zs
+right-split (right (right cmp x′∼y′) x∼y) _ with right-split (right cmp x′∼y′) _
+... | (_ , _ , eq₁ , eq₂) = -, -, refl ∷ eq₁ , x∼y ∷ eq₂
+right-split (front cmp w∼y) r with right-split cmp r
+... | (_ , _ , eq₁ , eq₂) = -, -, w∼y ∷ eq₁ , eq₂
+
+-- Eliminate equal splits
+
+eq-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → IsEqual cmp → ws ≋ ys × xs ≋ zs
+eq-split (back xs≋zs)    e = [] , xs≋zs
+eq-split (front cmp w∼y) e = map₁ (w∼y ∷_) (eq-split cmp e)