Complete proofs up to Proposition 3.2 (excluding unrolling)

7 files changed, 327 insertions, 236 deletions

diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index f0d1bb7..e1f7cc7 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -8,42 +8,34 @@ module Cfe.Language.Base
 
 open Setoid over using () renaming (Carrier to C)
 
-open import Cfe.Relation.Indexed
+open import Algebra
 open import Data.Empty
-open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid over
+open import Data.List hiding (null)
 open import Data.Product
+open import Data.Unit using (⊤; tt)
 open import Function hiding (Injection; Surjection; Inverse)
 import Function.Equality as Equality using (setoid)
 open import Level as L hiding (Lift)
 open import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial
-import Relation.Binary.PropositionalEquality as ≡
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 open import Relation.Binary.Indexed.Heterogeneous
 
+infix 4 _∈_
+
 Language : ∀ a aℓ → Set (suc c ⊔ suc a ⊔ suc aℓ)
 Language a aℓ = IndexedSetoid (List C) a aℓ
 
 ∅ : Language 0ℓ 0ℓ
 ∅ = Trivial.indexedSetoid (≡.setoid ⊥)
 
-｛ε｝ : Language (c ⊔ ℓ) (c ⊔ ℓ)
+｛ε｝ : Language c 0ℓ
 ｛ε｝ = record
-  { Carrier = [] ≋_
-  ; _≈_ = λ {l₁} {l₂} []≋l₁ []≋l₂ → ∃[ l₁≋l₂ ] (≋-trans []≋l₁ l₁≋l₂ ≡.≡ []≋l₂)
+  { Carrier = [] ≡_
+  ; _≈_ = λ _ _ → ⊤
   ; isEquivalence = record
-    { refl = λ {_} {x} →
-      ≋-refl ,
-      ( case x return (λ x → ≋-trans x ≋-refl ≡.≡ x) of λ {[] → ≡.refl} )
-    ; sym = λ {_} {_} {x} {y} (z , _) →
-      ≋-sym z ,
-      ( case (x , y , z)
-        return (λ (x , y , z) → ≋-trans y (≋-sym z) ≡.≡ x)
-        of λ {([] , [] , []) → ≡.refl} )
-    ; trans = λ {_} {_} {_} {v} {w} {x} (y , _) (z , _) →
-      ≋-trans y z ,
-      ( case (v , w , x , y , z)
-        return (λ (v , _ , x , y , z) → ≋-trans v (≋-trans y z) ≡.≡ x)
-        of λ {([] , [] , [] , [] , []) → ≡.refl} )
+    { refl = tt
+    ; sym = λ _ → tt
+    ; trans = λ _ _ → tt
     }
   }
 
@@ -66,6 +58,9 @@ Lift b bℓ A = record
 _∈_ : ∀ {a aℓ} → List C → Language a aℓ → Set a
 _∈_ = flip 𝕃
 
+∈-cong : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → l₁ ≡ l₂ → l₁ ∈ A → l₂ ∈ A
+∈-cong A ≡.refl l∈A = l∈A
+
 ≈ᴸ : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → 𝕃 A l₁ → 𝕃 A l₂ → Set aℓ
 ≈ᴸ = IndexedSetoid._≈_
 
@@ -78,6 +73,13 @@ _∈_ = flip 𝕃
 ≈ᴸ-trans : ∀ {a aℓ} → (A : Language a aℓ) → Transitive (𝕃 A) (≈ᴸ A)
 ≈ᴸ-trans = IsIndexedEquivalence.trans ∘ IndexedSetoid.isEquivalence
 
+≈ᴸ-cong : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂ l₃ l₄} →
+          (l₁≡l₂ : l₁ ≡ l₂) → (l₃≡l₄ : l₃ ≡ l₄) →
+          (l₁∈A : l₁ ∈ A) → (l₃∈A : l₃ ∈ A) →
+          ≈ᴸ A l₁∈A l₃∈A →
+          ≈ᴸ A (∈-cong A l₁≡l₂ l₁∈A) (∈-cong A l₃≡l₄ l₃∈A)
+≈ᴸ-cong A ≡.refl ≡.refl l₁∈A l₃∈A eq = eq
+
 record _≤_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where
   field
     f : ∀ {l} → l ∈ A → l ∈ B
@@ -119,23 +121,30 @@ record _≈_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (
   module A≈B = _≈_ A≈B
   module B≈C = _≈_ B≈C
 
-setoid : ∀ a aℓ → B.Setoid (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ)
-setoid a aℓ = record
-  { Carrier = Language a aℓ
-  ; _≈_ = _≈_
-  ; isEquivalence = record
-    { refl = ≈-refl
-    ; sym = ≈-sym
-    ; trans = ≈-trans
-    }
+≈-isEquivalence : ∀ {a aℓ} → B.IsEquivalence (_≈_ {a} {aℓ} {a} {aℓ})
+≈-isEquivalence = record
+  { refl = ≈-refl
+  ; sym = ≈-sym
+  ; trans = ≈-trans
   }
 
+setoid : ∀ a aℓ → B.Setoid (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ)
+setoid a aℓ = record { isEquivalence = ≈-isEquivalence {a} {aℓ} }
+
 ≤-refl : ∀ {a aℓ} → B.Reflexive (_≤_ {a} {aℓ})
 ≤-refl = record
   { f = id
   ; cong = id
   }
 
+≤-reflexive : ∀ {a aℓ b bℓ} → _≈_ {a} {aℓ} {b} {bℓ} B.⇒ _≤_
+≤-reflexive A≈B = record
+  { f = A≈B.f
+  ; cong = A≈B.cong₁
+  }
+  where
+  module A≈B = _≈_ A≈B
+
 ≤-trans : ∀ {a aℓ b bℓ c cℓ} → B.Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_
 ≤-trans A≤B B≤C = record
   { f = B≤C.f ∘ A≤B.f
@@ -161,3 +170,25 @@ setoid a aℓ = record
   { f = λ ()
   ; cong = λ {_} {_} {}
   }
+
+≤-isPartialOrder : ∀ a aℓ → B.IsPartialOrder (_≈_ {a} {aℓ}) _≤_
+≤-isPartialOrder a aℓ = record
+  { isPreorder = record
+    { isEquivalence = ≈-isEquivalence
+    ; reflexive = ≤-reflexive
+    ; trans = ≤-trans
+    }
+  ; antisym = ≤-antisym
+  }
+
+poset : ∀ a aℓ → B.Poset (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ) (c ⊔ a ⊔ aℓ)
+poset a aℓ = record { isPartialOrder = ≤-isPartialOrder a aℓ }
+
+null : ∀ {a} {aℓ} → Language a aℓ → Set a
+null A = [] ∈ A
+
+first : ∀ {a} {aℓ} → Language a aℓ → C → Set (c ⊔ a)
+first A x = ∃[ l ] x ∷ l ∈ A
+
+flast : ∀ {a} {aℓ} → Language a aℓ → C → Set (c ⊔ a)
+flast A x = ∃[ l ] (l ≡.≢ [] × ∃[ l′ ] l ++ x ∷ l′ ∈ A)
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index 29e635d..62acf8f 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -1,40 +1,128 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary
-import Cfe.Language
 
 module Cfe.Language.Construct.Concatenate
-  {c ℓ a aℓ b bℓ} (over : Setoid c ℓ)
-  (A : Cfe.Language.Language over a aℓ)
-  (B : Cfe.Language.Language over b bℓ)
+  {c ℓ} (over : Setoid c ℓ)
   where
 
+open import Algebra
+open import Cfe.Language over as 𝕃
 open import Data.Empty
 open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid over
+open import Data.List.Properties
 open import Data.Product as Product
 open import Function
 open import Level
-open import Cfe.Language over
+open import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.Indexed.Heterogeneous as I
 
-open Setoid over renaming (Carrier to C)
+open Setoid over using () renaming (Carrier to C)
 
-infix 4 _≈ᶜ_
-infix 4 _∙_
+module _
+  {a aℓ b bℓ}
+  (A : Language a aℓ)
+  (B : Language b bℓ)
+  where
+
+  infix 4 _≈ᶜ_
+  infix 4 _∙_
+
+  Concat : List C → Set (c ⊔ a ⊔ b)
+  Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B ×  l₁ ++ l₂ ≡ l
 
-Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
-Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B ×  l₁ ++ l₂ ≋ l
+  _≈ᶜ_ : {l₁ l₂ : List C} → REL (Concat l₁) (Concat l₂) (aℓ ⊔ bℓ)
+  (_ , l₁∈A , _ , l₂∈B , _) ≈ᶜ (_ , l₁′∈A , _ , l₂′∈B , _) = (≈ᴸ A l₁∈A l₁′∈A) × (≈ᴸ B l₂∈B l₂′∈B)
 
-_≈ᶜ_ : {l₁ l₂ : List C} → REL (Concat l₁) (Concat l₂) (aℓ ⊔ bℓ)
-(_ , l₁∈A , _ , l₂∈B , _) ≈ᶜ (_ , l₁′∈A , _ , l₂′∈B , _) = (≈ᴸ A l₁∈A l₁′∈A) × (≈ᴸ B l₂∈B l₂′∈B)
+  _∙_ : Language (c ⊔ a ⊔ b) (aℓ ⊔ bℓ)
+  _∙_ = record
+    { Carrier = Concat
+    ; _≈_ = _≈ᶜ_
+    ; isEquivalence = record
+      { refl = ≈ᴸ-refl A , ≈ᴸ-refl B
+      ; sym = Product.map (≈ᴸ-sym A) (≈ᴸ-sym B)
+      ; trans = Product.zip (≈ᴸ-trans A) (≈ᴸ-trans B)
+      }
+    }
 
-_∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b) (aℓ ⊔ bℓ)
-_∙_ = record
-  { Carrier = Concat
-  ; _≈_ = _≈ᶜ_
-  ; isEquivalence = record
-    { refl = ≈ᴸ-refl A , ≈ᴸ-refl B
-    ; sym = Product.map (≈ᴸ-sym A) (≈ᴸ-sym B)
-    ; trans = Product.zip (≈ᴸ-trans A) (≈ᴸ-trans B)
+isMonoid : ∀ {a aℓ} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)
+isMonoid {a} = record
+  { isSemigroup = record
+    { isMagma = record
+      { isEquivalence = ≈-isEquivalence
+      ; ∙-cong = λ X≈Y U≈V → record
+        { f = λ { (l₁ , l₁∈X , l₂ , l₂∈U , l₁++l₂≡l) → l₁ , _≈_.f X≈Y l₁∈X , l₂ , _≈_.f U≈V l₂∈U , l₁++l₂≡l}
+        ; f⁻¹ = λ { (l₁ , l₁∈Y , l₂ , l₂∈V , l₁++l₂≡l) → l₁ , _≈_.f⁻¹ X≈Y l₁∈Y , l₂ , _≈_.f⁻¹ U≈V l₂∈V , l₁++l₂≡l}
+        ; cong₁ = λ { (x , y) → _≈_.cong₁ X≈Y x ,  _≈_.cong₁ U≈V y}
+        ; cong₂ = λ { (x , y) → _≈_.cong₂ X≈Y x ,  _≈_.cong₂ U≈V y}
+        }
+      }
+    ; assoc = λ X Y Z → record
+      { f = λ {l} → (λ { (l₁ , (l₁′ , l₁′∈X , l₂′ , l₂′∈Y , l₁′++l₂′≡l₁) , l₂ , l₂∈Z , l₁++l₂≡l) →
+        l₁′ , l₁′∈X , l₂′ ++ l₂ , (l₂′ , l₂′∈Y , l₂ , l₂∈Z , refl) , (begin
+          l₁′ ++ l₂′ ++ l₂   ≡˘⟨ ++-assoc l₁′ l₂′ l₂ ⟩
+          (l₁′ ++ l₂′) ++ l₂ ≡⟨ cong (_++ l₂) l₁′++l₂′≡l₁ ⟩
+          l₁ ++ l₂          ≡⟨ l₁++l₂≡l ⟩
+          l                 ∎)})
+      ; f⁻¹ = λ {l} → λ { (l₁ , l₁∈X , l₂ , (l₁′ , l₁′∈Y , l₂′ , l₂′∈Z , l₁′++l₂′≡l₂), l₁++l₂≡l) →
+        l₁ ++ l₁′ , ( l₁ , l₁∈X , l₁′ , l₁′∈Y , refl) , l₂′ , l₂′∈Z , (begin
+          (l₁ ++ l₁′) ++ l₂′ ≡⟨ ++-assoc l₁ l₁′ l₂′ ⟩
+          l₁ ++ (l₁′ ++ l₂′) ≡⟨ cong (l₁ ++_) l₁′++l₂′≡l₂ ⟩
+          l₁ ++ l₂          ≡⟨ l₁++l₂≡l ⟩
+          l                 ∎)}
+      ; cong₁ = Product.assocʳ
+      ; cong₂ = Product.assocˡ
+      }
     }
+  ; identity = (λ A → record
+    { f = idˡ {a} A
+    ; f⁻¹ = λ {l} l∈A → [] , lift refl , l , l∈A , refl
+    ; cong₁ = λ {l₁} {l₂} {l₁∈A} {l₂∈A} → idˡ-cong {a} A {l₁} {l₂} {l₁∈A} {l₂∈A}
+    ; cong₂ = λ l₁≈l₂ → lift _ , l₁≈l₂
+    }) , (λ A → record
+    { f = idʳ {a} A
+    ; f⁻¹ = λ {l} l∈A → l , l∈A , [] , lift refl , ++-identityʳ l
+    ; cong₁ = λ {l₁} {l₂} {l₁∈A} {l₂∈A} → idʳ-cong {a} A {l₁} {l₂} {l₁∈A} {l₂∈A}
+    ; cong₂ = λ l₁≈l₂ → l₁≈l₂ , lift _
+    })
+  }
+  where
+  open ≡.≡-Reasoning
+
+  idˡ : ∀ {a aℓ} →
+        (A : Language (c ⊔ ℓ ⊔ a) aℓ) →
+        ∀ {l} →
+        l ∈ ((𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) ∙ A) →
+        l ∈ A
+  idˡ _ ([] , _ , l , l∈A , refl) = l∈A
+
+  idˡ-cong : ∀ {a aℓ} →
+             (A : Language (c ⊔ ℓ ⊔ a) aℓ) →
+             ∀ {l₁ l₂ l₁∈A l₂∈A} →
+             ≈ᴸ ((𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) ∙ A) {l₁} {l₂} l₁∈A l₂∈A →
+             ≈ᴸ A (idˡ {a} A l₁∈A) (idˡ {a} A l₂∈A)
+  idˡ-cong _ {l₁∈A = [] , _ , l₁ , l₁∈A , refl} {[] , _ , l₂ , l₂∈A , refl} (_ , l₁≈l₂) = l₁≈l₂
+
+  idʳ : ∀ {a aℓ} →
+        (A : Language (c ⊔ ℓ ⊔ a) aℓ) →
+        ∀ {l} →
+        l ∈ (A ∙ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)) →
+        l ∈ A
+  idʳ A (l , l∈A , [] , _ , refl) = ∈-cong A (sym (++-identityʳ l)) l∈A
+
+  idʳ-cong : ∀ {a aℓ} →
+             (A : Language (c ⊔ ℓ ⊔ a) aℓ) →
+             ∀ {l₁ l₂ l₁∈A l₂∈A} →
+             ≈ᴸ (A ∙ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)) {l₁} {l₂} l₁∈A l₂∈A →
+             ≈ᴸ A (idʳ {a} A l₁∈A) (idʳ {a} A l₂∈A)
+  idʳ-cong A {l₁∈A = l₁ , l₁∈A , [] , _ , refl} {l₂ , l₂∈A , [] , _ , refl} (l₁≈l₂ , _) =
+    ≈ᴸ-cong A (sym (++-identityʳ l₁)) (sym (++-identityʳ l₂)) l₁∈A l₂∈A l₁≈l₂
+
+∙-monotone : ∀ {a aℓ b bℓ} → _∙_ Preserves₂ _≤_ {a} {aℓ} ⟶ _≤_ {b} {bℓ} ⟶ _≤_
+∙-monotone X≤Y U≤V = record
+  { f = λ {(_ , l₁∈X , _ , l₂∈U , l₁++l₂≡l) → -, X≤Y.f l₁∈X , -, U≤V.f l₂∈U , l₁++l₂≡l}
+  ; cong = Product.map X≤Y.cong U≤V.cong
   }
+  where
+  module X≤Y = _≤_ X≤Y
+  module U≤V = _≤_ U≤V
diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda
index daa1628..b06be3d 100644
--- a/src/Cfe/Language/Construct/Single.agda
+++ b/src/Cfe/Language/Construct/Single.agda
@@ -6,70 +6,23 @@ import Relation.Binary.PropositionalEquality as ≡
 
 module Cfe.Language.Construct.Single
   {c ℓ} (over : Setoid c ℓ)
-  (≈-trans-bijₗ : ∀ {a b c b≈c}
-                  → Bijective ≡._≡_ ≡._≡_ (flip (Setoid.trans over {a} {b} {c}) b≈c))
-  (≈-trans-reflₗ : ∀ {a b a≈b}
-                   → Setoid.trans over {a} a≈b (Setoid.refl over {b}) ≡.≡ a≈b)
-  (≈-trans-symₗ : ∀ {a b c a≈b a≈c b≈c}
-                  → Setoid.trans over {a} {b} {c} a≈b b≈c ≡.≡ a≈c
-                  → Setoid.trans over a≈c (Setoid.sym over b≈c) ≡.≡ a≈b)
-  (≈-trans-transₗ : ∀ {a b c d a≈b a≈c a≈d b≈c c≈d}
-                  → Setoid.trans over {a} {b} a≈b b≈c ≡.≡ a≈c
-                  → Setoid.trans over {a} {c} {d} a≈c c≈d ≡.≡ a≈d
-                  → Setoid.trans over a≈b (Setoid.trans over b≈c c≈d) ≡.≡ a≈d)
   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
 
-private
-  ∷-inj : {a b : C} {l₁ l₂ : List C} {a≈b a≈b′ : a ≈ b} {l₁≋l₂ l₁≋l₂′ : l₁ ≋ l₂} → ≡._≡_ {A = a ∷ l₁ ≋ b ∷ l₂} (a≈b ∷ l₁≋l₂) (a≈b′ ∷ l₁≋l₂′) → (a≈b ≡.≡ a≈b′) × (l₁≋l₂ ≡.≡ l₁≋l₂′)
-  ∷-inj ≡.refl = ≡.refl , ≡.refl
-
-  ≋-trans-injₗ : {x l₁ l₂ : List C} → {l₁≋l₂ : l₁ ≋ l₂} → Injective ≡._≡_ ≡._≡_ (flip (≋-trans {x}) l₁≋l₂)
-  ≋-trans-injₗ {_} {_} {_} {_} {[]} {[]} _ = ≡.refl
-  ≋-trans-injₗ {_} {_} {_} {_ ∷ _} {_ ∷ _} {_ ∷ _} = uncurry (≡.cong₂ _∷_)
-                                               ∘ Product.map (proj₁ ≈-trans-bijₗ) ≋-trans-injₗ
-                                               ∘ ∷-inj
-
-  ≋-trans-surₗ : {x l₁ l₂ : List C} → {l₁≋l₂ : l₁ ≋ l₂} → Surjective {A = x ≋ l₁} ≡._≡_ ≡._≡_ (flip (≋-trans {x}) l₁≋l₂)
-  ≋-trans-surₗ {_} {_} {_} {[]} [] = [] , ≡.refl
-  ≋-trans-surₗ {_} {_} {_} {_ ∷ _} (a≈c ∷ x≋l₂) = Product.zip _∷_ (≡.cong₂ _∷_) (proj₂ ≈-trans-bijₗ a≈c) (≋-trans-surₗ x≋l₂)
-
-  ≋-trans-reflₗ : {l₁ l₂ : List C} {l₁≋l₂ : l₁ ≋ l₂} → ≋-trans l₁≋l₂ ≋-refl ≡.≡ l₁≋l₂
-  ≋-trans-reflₗ {_} {_} {[]} = ≡.refl
-  ≋-trans-reflₗ {_} {_} {a≈b ∷ l₁≋l₂} = ≡.cong₂ _∷_ ≈-trans-reflₗ ≋-trans-reflₗ
-
-  ≋-trans-symₗ : {l₁ l₂ l₃ : List C} {l₁≋l₂ : l₁ ≋ l₂} {l₁≋l₃ : l₁ ≋ l₃} {l₂≋l₃ : l₂ ≋ l₃}
-               → ≋-trans l₁≋l₂ l₂≋l₃ ≡.≡ l₁≋l₃
-               → ≋-trans l₁≋l₃ (≋-sym l₂≋l₃) ≡.≡ l₁≋l₂
-  ≋-trans-symₗ {_} {_} {_} {[]} {[]} {[]} _ = ≡.refl
-  ≋-trans-symₗ {_} {_} {_} {_ ∷ _} {_ ∷ _} {_ ∷ _} = uncurry (≡.cong₂ _∷_)
-                                                   ∘ Product.map ≈-trans-symₗ ≋-trans-symₗ
-                                                   ∘ ∷-inj
-
-  ≋-trans-transₗ : {l₁ l₂ l₃ l₄ : List C}
-                 → {l₁≋l₂ : l₁ ≋ l₂} {l₁≋l₃ : l₁ ≋ l₃} {l₁≋l₄ : l₁ ≋ l₄} {l₂≋l₃ : l₂ ≋ l₃} {l₃≋l₄ : l₃ ≋ l₄}
-                 → ≋-trans l₁≋l₂ l₂≋l₃ ≡.≡ l₁≋l₃
-                 → ≋-trans l₁≋l₃ l₃≋l₄ ≡.≡ l₁≋l₄
-                 → ≋-trans l₁≋l₂ (≋-trans l₂≋l₃ l₃≋l₄) ≡.≡ l₁≋l₄
-  ≋-trans-transₗ {l₁≋l₂ = []} {[]} {[]} {[]} {[]} _ _ = ≡.refl
-  ≋-trans-transₗ {l₁≋l₂ = _ ∷ _} {_ ∷ _} {_ ∷ _} {_ ∷ _} {_ ∷ _} = uncurry (≡.cong₂ _∷_)
-                                                                 ∘₂ uncurry (Product.zip ≈-trans-transₗ ≋-trans-transₗ)
-                                                                 ∘₂ curry (Product.map ∷-inj ∷-inj)
-
-｛_｝ : C → Language (c ⊔ ℓ) (c ⊔ ℓ)
+｛_｝ : C → Language (c ⊔ ℓ) 0ℓ
 ｛ c ｝ = record
-  { Carrier = [ c ] ≋_
-  ; _≈_ = λ l≋m l≋n → ∃[ m≋n ] ≋-trans l≋m m≋n ≡.≡ l≋n
+  { Carrier = λ l → ∃[ a ] (l ≡.≡ [ a ] × a ≈ c)
+  ; _≈_ = λ _ _ → ⊤
   ; isEquivalence = record
-    { refl = ≋-refl , ≋-trans-reflₗ
-    ; sym = Product.map ≋-sym ≋-trans-symₗ
-    ; trans = Product.zip ≋-trans ≋-trans-transₗ
+    { refl = tt
+    ; sym = λ _ → tt
+    ; trans = λ _ _ → tt
     }
   }
diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda
index ee8b0f7..4ed0774 100644
--- a/src/Cfe/Language/Construct/Union.agda
+++ b/src/Cfe/Language/Construct/Union.agda
@@ -1,14 +1,12 @@
 {-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary
-import Cfe.Language
 
 module Cfe.Language.Construct.Union
-  {c ℓ a aℓ b bℓ} (over : Setoid c ℓ)
-  (A : Cfe.Language.Language over a aℓ)
-  (B : Cfe.Language.Language over b bℓ)
+  {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
@@ -16,44 +14,82 @@ open import Data.Product as Product
 open import Data.Sum as Sum
 open import Function
 open import Level
-open import Cfe.Language over hiding (Lift)
+open import Cfe.Language over as 𝕃 hiding (Lift)
 
 open Setoid over renaming (Carrier to C)
 
-infix 4 _≈ᵁ_
-infix 4 _∪_
-
-Union : List C → Set (a ⊔ b)
-Union l = l ∈ A ⊎ l ∈ B
-
-_≈ᵁ_ : {l₁ l₂ : List C} → REL (Union l₁) (Union l₂) (aℓ ⊔ bℓ)
-(inj₁ x) ≈ᵁ (inj₁ y) = Lift bℓ (≈ᴸ A x y)
-(inj₁ _) ≈ᵁ (inj₂ _) = Lift (aℓ ⊔ bℓ) ⊥
-(inj₂ _) ≈ᵁ (inj₁ _) = Lift (aℓ ⊔ bℓ) ⊥
-(inj₂ x) ≈ᵁ (inj₂ y) = Lift aℓ (≈ᴸ B x y)
-
-_∪_ : Language (a ⊔ b) (aℓ ⊔ bℓ)
-_∪_ = record
-  { Carrier = Union
-  ; _≈_ = _≈ᵁ_
-  ; isEquivalence = record
-    { refl = λ {_} {x} → case x return (λ x → x ≈ᵁ x) of λ
-      { (inj₁ x) → lift (≈ᴸ-refl A)
-      ; (inj₂ y) → lift (≈ᴸ-refl B)
+module _
+  {a aℓ b bℓ}
+  (A : Language a aℓ)
+  (B : Language b bℓ)
+  where
+
+  infix 4 _≈ᵁ_
+  infix 4 _∪_
+
+  Union : List C → Set (a ⊔ b)
+  Union l = l ∈ A ⊎ l ∈ B
+
+  data _≈ᵁ_ : {l₁ l₂ : List C} → REL (Union l₁) (Union l₂) (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where
+    A≈A : ∀ {l₁ l₂ x y} → ≈ᴸ A {l₁} {l₂} x y → (inj₁ x) ≈ᵁ (inj₁ y)
+    B≈B : ∀ {l₁ l₂ x y} → ≈ᴸ B {l₁} {l₂} x y → (inj₂ x) ≈ᵁ (inj₂ y)
+
+  _∪_ : Language (a ⊔ b) (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ)
+  _∪_ = record
+    { Carrier = Union
+    ; _≈_ = _≈ᵁ_
+    ; isEquivalence = record
+      { refl = λ {_} {x} → case x return (λ x → x ≈ᵁ x) of λ { (inj₁ x) → A≈A (≈ᴸ-refl A) ; (inj₂ y) → B≈B (≈ᴸ-refl B)}
+      ; sym = λ { (A≈A x) → A≈A (≈ᴸ-sym A x) ; (B≈B x) → B≈B (≈ᴸ-sym B x)}
+      ; trans = λ { (A≈A x) (A≈A y) → A≈A (≈ᴸ-trans A x y) ; (B≈B x) (B≈B y) → B≈B (≈ᴸ-trans B x y) }
       }
-    ; sym = λ {_} {_} {x} {y} x≈ᵁy →
-      case (∃[ x ] ∃[ y ] x ≈ᵁ y ∋ x , y , x≈ᵁy)
-      return (λ (x , y , _) → y ≈ᵁ x) of λ
-        { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (≈ᴸ-sym A x≈ᵁy)
-        ; (inj₂ y₁ , inj₂ y , lift x≈ᵁy) → lift (≈ᴸ-sym B x≈ᵁy)
+    }
+
+isCommutativeMonoid : ∀ {a aℓ} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a (c ⊔ a ⊔ 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)
+          ; cong₁ = λ { (A≈A x) → A≈A (_≈_.cong₁ X≈Y x) ; (B≈B x) → B≈B (_≈_.cong₁ U≈V x) }
+          ; cong₂ = λ { (A≈A x) → A≈A (_≈_.cong₂ X≈Y x) ; (B≈B x) → B≈B (_≈_.cong₂ U≈V x) }
+          }
         }
-    ; trans = λ {_} {_} {_} {x} {y} {z} x≈ᵁy y≈ᵁz →
-      case ∃[ x ] ∃[ y ] ∃[ z ] x ≈ᵁ y × y ≈ᵁ z ∋ x , y , z , x≈ᵁy , y≈ᵁz
-      return (λ (x , _ , z , _) → x ≈ᵁ z) of λ
-        { (inj₁ _ , inj₁ _ , inj₁ _ , lift x≈ᵁy , lift y≈ᵁz) →
-          lift (≈ᴸ-trans A x≈ᵁy y≈ᵁz)
-        ; (inj₂ _ , inj₂ _ , inj₂ _ , lift x≈ᵁy , lift y≈ᵁz) →
-          lift (≈ᴸ-trans B x≈ᵁy y≈ᵁz)
+      ; assoc = λ A B C → record
+        { f = Sum.assocʳ
+        ; f⁻¹ = Sum.assocˡ
+        ; cong₁ = λ { (A≈A (A≈A x)) → A≈A x ; (A≈A (B≈B x)) → B≈B (A≈A x) ; (B≈B x) → B≈B (B≈B x) }
+        ; cong₂ = λ { (A≈A x) → A≈A (A≈A x) ; (B≈B (A≈A x)) → A≈A (B≈B x) ; (B≈B (B≈B x)) → B≈B x }
         }
+      }
+    ; identity = (λ A → record
+      { f = λ { (inj₂ x) → x }
+      ; f⁻¹ = inj₂
+      ; cong₁ = λ { (B≈B x) → x }
+      ; cong₂ = B≈B
+      }) , (λ A → record
+      { f = λ { (inj₁ x) → x }
+      ; f⁻¹ = inj₁
+      ; cong₁ = λ { (A≈A x) → x }
+      ; cong₂ = A≈A
+      })
+    }
+  ; comm = λ A B → record
+    { f = Sum.swap
+    ; f⁻¹ = Sum.swap
+    ; cong₁ = λ { (A≈A x) → B≈B x ; (B≈B x) → A≈A x }
+    ; cong₂ = λ { (A≈A x) → B≈B x ; (B≈B x) → A≈A x }
     }
   }
+
+∪-monotone : ∀ {a aℓ b bℓ} → _∪_ Preserves₂ _≤_ {a} {aℓ} ⟶ _≤_ {b} {bℓ} ⟶ _≤_
+∪-monotone X≤Y U≤V = record
+  { f = Sum.map X≤Y.f U≤V.f
+  ; cong = λ { (A≈A l₁≈l₂) → A≈A (X≤Y.cong l₁≈l₂) ; (B≈B l₁≈l₂) → B≈B (U≤V.cong l₁≈l₂)}
+  }
+  where
+  module X≤Y = _≤_ X≤Y
+  module U≤V = _≤_ U≤V
diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
index 62a946e..3a78bd8 100644
--- a/src/Cfe/Language/Indexed/Construct/Iterate.agda
+++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda
@@ -8,10 +8,10 @@ module Cfe.Language.Indexed.Construct.Iterate
 
 open Setoid over using () renaming (Carrier to C)
 
-open import Cfe.Language over
+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.Nat as ℕ hiding (_⊔_; _≤_)
 open import Data.Product as Product
 open import Function
 open import Level hiding (Lift) renaming (suc to lsuc)
@@ -24,47 +24,85 @@ iter : ∀ {a} {A : Set a} → (A → A) → ℕ → A → A
 iter f ℕ.zero = id
 iter f (ℕ.suc n) = f ∘ iter f n
 
-Iterate : ∀ {a aℓ} → (Language a aℓ → Language a aℓ) → IndexedLanguage 0ℓ 0ℓ a aℓ
-Iterate {a} {aℓ} f = record
-  { Carrierᵢ = ℕ
-  ; _≈ᵢ_ = ≡._≡_
-  ; isEquivalenceᵢ = ≡.isEquivalence
-  ; F = λ n → iter f n (Lift a aℓ ∅)
-  ; cong = λ {≡.refl → ≈-refl}
-  }
-
-≈ᵗ-refl : ∀ {a aℓ} →
-          (g : Language a aℓ → Language a aℓ) →
-          Reflexive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
-≈ᵗ-refl g {_} {n , _} = refl , (≈ᴸ-refl (Iter.F n))
+f-fn-x≡fn-f-x : ∀ {a} {A : Set a} (f : A → A) n x → f (iter f n x) ≡ iter 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
-  module Iter = IndexedLanguage (Iterate g)
 
-≈ᵗ-sym : ∀ {a aℓ} →
-         (g : Language a aℓ → Language a aℓ) →
-         Symmetric (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
-≈ᵗ-sym g {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) =
-  refl , (≈ᴸ-sym (Iter.F n) x∈Fn≈y∈Fn)
+  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 → iter f n x A.≈ iter 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
-  module Iter = IndexedLanguage (Iterate g)
 
-≈ᵗ-trans : ∀ {a aℓ} →
-          (g : Language a aℓ → Language a aℓ) →
-          Transitive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
-≈ᵗ-trans g {_} {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) (refl , y∈Fn≈z∈Fn) =
-  refl , (≈ᴸ-trans (Iter.F n) x∈Fn≈y∈Fn y∈Fn≈z∈Fn)
+  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 → iter f n x A′.≤ iter 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ℓ}
   where
-  module Iter = IndexedLanguage (Iterate g)
-
-⋃ : ∀ {a aℓ} → (Language a aℓ → Language a aℓ) → Language a aℓ
-⋃ f = record
-  { Carrier = Iter.Tagged
-  ; _≈_ = Iter._≈ᵗ_
-  ; isEquivalence = record
-    { refl = ≈ᵗ-refl f
-    ; sym = ≈ᵗ-sym f
-    ; trans = ≈ᵗ-trans f
+  Iterate : (Language a aℓ → Language a aℓ) → IndexedLanguage 0ℓ 0ℓ a aℓ
+  Iterate f = record
+    { Carrierᵢ = ℕ
+    ; _≈ᵢ_ = ≡._≡_
+    ; isEquivalenceᵢ = ≡.isEquivalence
+    ; F = λ n → iter f n (Lift a aℓ ∅)
+    ; cong = λ {≡.refl → ≈-refl}
+    }
+
+  ≈ᵗ-refl : (g : Language a aℓ → Language a aℓ) →
+            Reflexive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
+  ≈ᵗ-refl g {_} {n , _} = refl , (≈ᴸ-refl (Iter.F n))
+    where
+    module Iter = IndexedLanguage (Iterate g)
+
+  ≈ᵗ-sym : (g : Language a aℓ → Language a aℓ) →
+           Symmetric (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
+  ≈ᵗ-sym g {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) =
+    refl , (≈ᴸ-sym (Iter.F n) x∈Fn≈y∈Fn)
+    where
+    module Iter = IndexedLanguage (Iterate g)
+
+  ≈ᵗ-trans : (g : Language a aℓ → Language a aℓ) →
+             Transitive (Tagged (Iterate g)) (_≈ᵗ_ (Iterate g))
+  ≈ᵗ-trans g {_} {_} {_} {n , _} (refl , x∈Fn≈y∈Fn) (refl , y∈Fn≈z∈Fn) =
+    refl , (≈ᴸ-trans (Iter.F n) x∈Fn≈y∈Fn y∈Fn≈z∈Fn)
+    where
+    module Iter = IndexedLanguage (Iterate g)
+
+  ⋃ : (Language a aℓ → Language a aℓ) → Language a aℓ
+  ⋃ f = record
+    { Carrier = Iter.Tagged
+    ; _≈_ = Iter._≈ᵗ_
+    ; isEquivalence = record
+      { refl = ≈ᵗ-refl f
+      ; sym = ≈ᵗ-sym f
+      ; trans = ≈ᵗ-trans f
+      }
+    }
+    where
+    module Iter = IndexedLanguage (Iterate f)
+
+  ⋃-cong : ∀ {f g : Language a aℓ → Language a aℓ} → (∀ {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 aℓ) f≈g n (Lift a aℓ ∅)) l∈fn}
+    ; f⁻¹ = λ { (n , l∈gn) → n , _≈_.f⁻¹ (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g n (Lift a aℓ ∅)) l∈gn}
+    ; cong₁ = λ {_} {_} {(i , _)} → λ { (refl , l₁≈l₂) → refl , _≈_.cong₁ (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g i (Lift a aℓ ∅)) l₁≈l₂}
+    ; cong₂ = λ {_} {_} {(i , _)} → λ { (refl , l₁≈l₂) → refl , _≈_.cong₂ (f≈g⇒fn≈gn (L.setoid a aℓ) f≈g i (Lift a aℓ ∅)) l₁≈l₂}
+    }
+
+  ⋃-monotone : ∀ {f g : Language a aℓ → Language a aℓ} → (∀ {x y} → x ≤ y → f x ≤ g y) → ⋃ f ≤ ⋃ g
+  ⋃-monotone f≤g = record
+    { f = λ { (n , l∈fn) → n , _≤_.f (f≤g⇒fn≤gn (poset a aℓ) f≤g n (Lift a aℓ ∅)) l∈fn }
+    ; cong = λ {_} {_} {(i , _)} → λ { (refl , l₁≈l₂) → refl , _≤_.cong (f≤g⇒fn≤gn (poset a aℓ) f≤g i (Lift a aℓ ∅)) l₁≈l₂ }
     }
-  }
-  where
-  module Iter = IndexedLanguage (Iterate f)
diff --git a/src/Cfe/Language/Indexed/Homogeneous.agda b/src/Cfe/Language/Indexed/Homogeneous.agda
index c032978..a1e284a 100644
--- a/src/Cfe/Language/Indexed/Homogeneous.agda
+++ b/src/Cfe/Language/Indexed/Homogeneous.agda
@@ -31,17 +31,3 @@ record IndexedLanguage i iℓ a aℓ : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a
 
   _≈ᵗ_ : IRel Tagged (iℓ ⊔ aℓ)
   _≈ᵗ_ (i , l∈Fi) (j , m∈Fj) = Σ (i ≈ᵢ j) λ i≈j → ≈ᴸ (F j) (f (cong i≈j) l∈Fi) m∈Fj
-
-  -- ≈ᵗ-refl : Reflexive Tagged _≈ᵗ_
-  -- ≈ᵗ-refl {l} {i , l∈Fi} = reflᵢ , {!≈ᴸ-refl!}
-
-  -- ⋃ : Language (i ⊔ a) (iℓ ⊔ aℓ)
-  -- ⋃ = record
-  --   { Carrier = Tagged
-  --   ; _≈_ = _≈ᵗ_
-  --   ; isEquivalence = record
-  --     { refl = λ i≈j → {!!}
-  --     ; sym = {!!}
-  --     ; trans = {!!}
-  --     }
-  --   }
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
deleted file mode 100644
index 52d4644..0000000
--- a/src/Cfe/Language/Properties.agda
+++ /dev/null
@@ -1,41 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Relation.Binary
-
-module Cfe.Language.Properties
-  {c ℓ} {setoid : Setoid c ℓ}
-  where
-
-open Setoid setoid renaming (Carrier to A)
-open import Cfe.Language setoid
-open Language
-
-open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid setoid
-open import Function
-open import Level
-open import Relation.Binary.Construct.InducedPoset
-
-_≤′_ : ∀ {a aℓ} → Rel (Language a aℓ) (c ⊔ a)
-_≤′_ = _≤_
-
-------------------------------------------------------------------------
--- Properties of _≤_
-
-≤-refl : ∀ {a aℓ} → Reflexive (_≤′_ {a} {aℓ})
-≤-refl = id
-
-≤-trans : ∀ {a b c aℓ bℓ cℓ} → Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_
-≤-trans A≤B B≤C = B≤C ∘ A≤B
-
-≤-poset : ∀ {a aℓ} → Poset (c ⊔ ℓ ⊔ suc (a ⊔ aℓ)) (c ⊔ a) (c ⊔ a)
-≤-poset {a} {aℓ} = InducedPoset (_≤′_ {a} {aℓ}) id (λ i≤j j≤k → j≤k ∘ i≤j)
-
--- ------------------------------------------------------------------------
--- -- Properties of _∪_
-
--- ∪-cong-≤ : Congruent₂ _≤_ _∪_
--- ∪-cong-≤ A≤B C≤D = map A≤B C≤D
-
--- ∪-cong : Congruent₂ _≈_ _∪_
--- ∪-cong {A} {B} {C} {D} = ≤-cong₂→≈-cong₂ {_∪_} (λ A≤B C≤D → map A≤B C≤D) {A} {B} {C} {D}