Change Language definition to respects instead of custom congruence.

7 files changed, 116 insertions, 255 deletions

diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index 74854df..bda9000 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 as B using (Setoid)
+open import Relation.Binary
 
 module Cfe.Language.Base
   {c ℓ} (over : Setoid c ℓ)
@@ -11,96 +11,61 @@ open Setoid over using () renaming (Carrier to C)
 open import Algebra
 open import Data.Empty
 open import Data.List hiding (null)
+open import Data.List.Relation.Binary.Equality.Setoid over
 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 Function hiding (_⟶_)
 open import Level as L hiding (Lift)
-open import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-open import Relation.Binary.Indexed.Heterogeneous
+open import Relation.Binary.PropositionalEquality
 
 infix 4 _∈_
 infix 4 _∉_
 
-Language : ∀ a aℓ → Set (suc c ⊔ suc a ⊔ suc aℓ)
-Language a aℓ = IndexedSetoid (List C) a aℓ
+record Language a : Set (c ⊔ ℓ ⊔ suc a) where
+  field
+    𝕃 : List C → Set a
+    ∈-resp-≋ : 𝕃 ⟶ 𝕃 Respects _≋_
 
-∅ : Language 0ℓ 0ℓ
-∅ = Trivial.indexedSetoid (≡.setoid ⊥)
+∅ : Language 0ℓ
+∅ = record
+  { 𝕃 = const ⊥
+  ; ∈-resp-≋ = λ _ ()
+  }
 
-｛ε｝ : Language c 0ℓ
+｛ε｝ : Language c
 ｛ε｝ = record
-  { Carrier = [] ≡_
-  ; _≈_ = λ _ _ → ⊤
-  ; isEquivalence = record
-    { refl = tt
-    ; sym = λ _ → tt
-    ; trans = λ _ _ → tt
-    }
+  { 𝕃 = [] ≡_
+  ; ∈-resp-≋ = λ { [] refl → refl}
   }
 
-Lift : ∀ {a aℓ} → (b bℓ : Level) → Language a aℓ → Language (a ⊔ b) (aℓ ⊔ bℓ)
-Lift b bℓ A = record
-  { Carrier = L.Lift b ∘ A.Carrier
-  ; _≈_ = λ (lift x) (lift y) → L.Lift bℓ (x A.≈ y)
-  ; isEquivalence = record
-    { refl = lift A.refl
-    ; sym = λ (lift x) → lift (A.sym x)
-    ; trans = λ (lift x) (lift y) → lift (A.trans x y)
-    }
+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)}
   }
   where
-  module A = IndexedSetoid A
-
-𝕃 : ∀ {a aℓ} → Language a aℓ → List C → Set a
-𝕃 = IndexedSetoid.Carrier
+  module A = Language A
 
-_∈_ : ∀ {a aℓ} → List C → Language a aℓ → Set a
-_∈_ = flip 𝕃
+_∈_ : ∀ {a} → List C → Language a → Set a
+_∈_ = flip Language.𝕃
 
-_∉_ : ∀ {a aℓ} → List C → Language a aℓ → Set a
+_∉_ : ∀ {a} → List C → Language a → Set a
 l ∉ A = l ∈ A → ⊥
 
-∈-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._≈_
-
-≈ᴸ-refl : ∀ {a aℓ} → (A : Language a aℓ) → Reflexive (𝕃 A) (≈ᴸ A)
-≈ᴸ-refl = IsIndexedEquivalence.refl ∘ IndexedSetoid.isEquivalence
-
-≈ᴸ-sym : ∀ {a aℓ} → (A : Language a aℓ) → Symmetric (𝕃 A) (≈ᴸ A)
-≈ᴸ-sym = IsIndexedEquivalence.sym ∘ IndexedSetoid.isEquivalence
-
-≈ᴸ-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
+record _≤_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ a ⊔ b) where
   field
     f : ∀ {l} → l ∈ A → l ∈ B
-    cong : ∀ {l₁ l₂ l₁∈A l₂∈A} → ≈ᴸ A {l₁} {l₂} l₁∈A l₂∈A → ≈ᴸ B (f l₁∈A) (f l₂∈A)
 
-record _≈_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (c ⊔ ℓ ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where
+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
-    cong₁ : ∀ {l₁ l₂ l₁∈A l₂∈A} → ≈ᴸ A {l₁} {l₂} l₁∈A l₂∈A → ≈ᴸ B (f l₁∈A) (f l₂∈A)
-    cong₂ : ∀ {l₁ l₂ l₁∈B l₂∈B} → ≈ᴸ B {l₁} {l₂} l₁∈B l₂∈B → ≈ᴸ A (f⁻¹ l₁∈B) (f⁻¹ l₂∈B)
 
-null : ∀ {a} {aℓ} → Language a aℓ → Set a
+null : ∀ {a} → Language a → Set a
 null A = [] ∈ A
 
-first : ∀ {a} {aℓ} → Language a aℓ → C → Set (c ⊔ a)
+first : ∀ {a} → Language 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)
+flast : ∀ {a} → Language 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 62acf8f..ef45432 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -10,6 +10,7 @@ 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
@@ -20,108 +21,65 @@ import Relation.Binary.Indexed.Heterogeneous as I
 open Setoid over using () renaming (Carrier to C)
 
 module _
-  {a aℓ b bℓ}
-  (A : Language a aℓ)
-  (B : Language b bℓ)
+  {a b}
+  (A : Language a)
+  (B : Language b)
   where
 
-  infix 4 _≈ᶜ_
-  infix 4 _∙_
+  module A = Language A
+  module B = Language B
 
-  Concat : List C → Set (c ⊔ a ⊔ b)
-  Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B ×  l₁ ++ l₂ ≡ l
+  infix 4 _∙_
 
-  _≈ᶜ_ : {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)
+  Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
+  Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≋ l
 
-  _∙_ : Language (c ⊔ a ⊔ b) (aℓ ⊔ bℓ)
+  _∙_ : Language (c ⊔ ℓ ⊔ 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)
+    { 𝕃 = Concat
+    ; ∈-resp-≋ = λ { l≋l′ (_ , l₁∈A , _ , l₂∈B , eq) → -, l₁∈A , -, l₂∈B , ≋-trans eq l≋l′
       }
     }
 
-isMonoid : ∀ {a aℓ} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)
+isMonoid : ∀ {a} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ 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}
+        { f = λ { (_ , l₁∈X , _ , l₂∈U , eq) → -, _≈_.f X≈Y l₁∈X , -, _≈_.f U≈V l₂∈U , eq }
+        ; f⁻¹ = λ { (_ , l₁∈Y , _ , l₂∈V , eq) → -, _≈_.f⁻¹ X≈Y l₁∈Y , -, _≈_.f⁻¹ U≈V l₂∈V , eq }
         }
       }
     ; 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ˡ
+      { f = λ {l} → λ { (l₁₂ , (l₁ , l₁∈X , l₂ , l₂∈Y , eq₁) , l₃ , l₃∈Z , eq₂) →
+        -, l₁∈X , -, (-, l₂∈Y , -, l₃∈Z , ≋-refl) , (begin
+          l₁ ++ l₂ ++ l₃ ≡˘⟨ ++-assoc l₁ l₂ l₃ ⟩
+          (l₁ ++ l₂) ++ l₃ ≈⟨ ++⁺ eq₁ ≋-refl ⟩
+          l₁₂ ++ l₃ ≈⟨ eq₂ ⟩
+          l ∎) }
+      ; f⁻¹ = λ {l} → λ { (l₁ , l₁∈X , l₂₃ , (l₂ , l₂∈Y , l₃ , l₃∈Z , eq₁) , eq₂) →
+        -, (-, l₁∈X , -, l₂∈Y , ≋-refl) , -, l₃∈Z , (begin
+          (l₁ ++ l₂) ++ l₃ ≡⟨ ++-assoc l₁ l₂ l₃ ⟩
+          l₁ ++ l₂ ++ l₃ ≈⟨ ++⁺ ≋-refl eq₁ ⟩
+          l₁ ++ l₂₃ ≈⟨ eq₂ ⟩
+          l ∎) }
       }
     }
-  ; 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 _
+  ; identity = (λ X → record
+    { f = λ { ([] , _ , _ , l₂∈X , eq) → Language.∈-resp-≋ X eq l₂∈X }
+    ; f⁻¹ = λ l∈X → -, lift refl , -, l∈X , ≋-refl
+    }) , (λ X → record
+    { f = λ { (l₁ , l₁∈X , [] , _ , eq) → Language.∈-resp-≋ X (≋-trans (≋-reflexive (sym (++-identityʳ l₁))) eq) l₁∈X }
+    ; f⁻¹ = λ {l} l∈X → -, l∈X , -, lift refl , ≋-reflexive (++-identityʳ l)
     })
   }
   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₂
+  open import Relation.Binary.Reasoning.Setoid ≋-setoid
 
-∙-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
+∙-mono : ∀ {a b} → _∙_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
+∙-mono X≤Y U≤V = record
+  { f = λ {(_ , l₁∈X , _ , l₂∈U , eq) → -, X≤Y.f l₁∈X , -, U≤V.f l₂∈U , eq}
   }
   where
   module X≤Y = _≤_ X≤Y
diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda
index b06be3d..ddea1a6 100644
--- a/src/Cfe/Language/Construct/Single.agda
+++ b/src/Cfe/Language/Construct/Single.agda
@@ -12,17 +12,16 @@ 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 ⊔ ℓ) 0ℓ
+｛_｝ : C → Language (c ⊔ ℓ)
 ｛ c ｝ = record
-  { Carrier = λ l → ∃[ a ] (l ≡.≡ [ a ] × a ≈ c)
-  ; _≈_ = λ _ _ → ⊤
-  ; isEquivalence = record
-    { refl = tt
-    ; sym = λ _ → tt
-    ; trans = λ _ _ → tt
-    }
+  { 𝕃 = [ 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
index 5099d04..5e86124 100644
--- a/src/Cfe/Language/Construct/Union.agda
+++ b/src/Cfe/Language/Construct/Union.agda
@@ -19,33 +19,26 @@ open import Cfe.Language over as 𝕃 hiding (Lift)
 open Setoid over renaming (Carrier to C)
 
 module _
-  {a aℓ b bℓ}
-  (A : Language a aℓ)
-  (B : Language b bℓ)
+  {a b}
+  (A : Language a)
+  (B : Language b)
   where
 
-  infix 4 _≈ᵁ_
+  module A = Language A
+  module B = Language B
+
   infix 6 _∪_
 
   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ℓ)
+  _∪_ : Language (a ⊔ 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) }
-      }
+    { 𝕃 = Union
+    ; ∈-resp-≋ = λ l₁≋l₂ → Sum.map (A.∈-resp-≋ l₁≋l₂) (B.∈-resp-≋ l₁≋l₂)
     }
 
-isCommutativeMonoid : ∀ {a aℓ} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a (c ⊔ a ⊔ aℓ) ∅)
+isCommutativeMonoid : ∀ {a} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a ∅)
 isCommutativeMonoid = record
   { isMonoid = record
     { isSemigroup = record
@@ -54,47 +47,36 @@ isCommutativeMonoid = record
         ; ∙-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) }
           }
         }
       ; 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
+∪-mono : ∀ {a b} → _∪_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
+∪-mono 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
 
-∪-unique : ∀ {a aℓ b bℓ} {A : Language a aℓ} {B : Language b 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 : ∀ {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)
diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
index 3a78bd8..5ed031b 100644
--- a/src/Cfe/Language/Indexed/Construct/Iterate.agda
+++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda
@@ -49,60 +49,32 @@ module _
   f≤g⇒fn≤gn f≤g (suc n) x = f≤g (f≤g⇒fn≤gn f≤g n x)
 
 module _
-  {a aℓ}
+  {a}
   where
-  Iterate : (Language a aℓ → Language a aℓ) → IndexedLanguage 0ℓ 0ℓ a aℓ
+  Iterate : (Language a → Language a) → IndexedLanguage 0ℓ 0ℓ a
   Iterate f = record
     { Carrierᵢ = ℕ
     ; _≈ᵢ_ = ≡._≡_
     ; isEquivalenceᵢ = ≡.isEquivalence
-    ; F = λ n → iter f n (Lift a aℓ ∅)
+    ; F = λ n → iter f n (Lift 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ℓ
+  ⋃ : (Language a → Language a) → Language a
   ⋃ f = record
-    { Carrier = Iter.Tagged
-    ; _≈_ = Iter._≈ᵗ_
-    ; isEquivalence = record
-      { refl = ≈ᵗ-refl f
-      ; sym = ≈ᵗ-sym f
-      ; trans = ≈ᵗ-trans f
-      }
+    { 𝕃 = Iter.Tagged
+    ; ∈-resp-≋ = λ { l₁≋l₂ (i , l₁∈fi) → i , Language.∈-resp-≋ (Iter.F i) l₁≋l₂ l₁∈fi }
     }
     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} → (∀ {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₂}
+    { 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}
     }
 
-  ⋃-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₂ }
+  ⋃-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
index a1e284a..44e3b6c 100644
--- a/src/Cfe/Language/Indexed/Homogeneous.agda
+++ b/src/Cfe/Language/Indexed/Homogeneous.agda
@@ -16,18 +16,15 @@ open _≈_
 
 open Setoid over using () renaming (Carrier to C)
 
-record IndexedLanguage i iℓ a aℓ : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a ⊔ aℓ)) where
+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 aℓ
+    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
-
-  _≈ᵗ_ : IRel Tagged (iℓ ⊔ aℓ)
-  _≈ᵗ_ (i , l∈Fi) (j , m∈Fj) = Σ (i ≈ᵢ j) λ i≈j → ≈ᴸ (F j) (f (cong i≈j) l∈Fi) m∈Fj
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index 325b410..b2630ce 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -15,87 +15,75 @@ open import Data.List.Relation.Binary.Equality.Setoid over
 open import Function
 open import Level
 
-≈-refl : ∀ {a aℓ} → Reflexive (_≈_ {a} {aℓ})
+≈-refl : ∀ {a} → Reflexive (_≈_ {a})
 ≈-refl {x = A} = record
   { f = id
   ; f⁻¹ = id
-  ; cong₁ = id
-  ; cong₂ = id
   }
 
-≈-sym : ∀ {a aℓ b bℓ} → Sym (_≈_ {a} {aℓ} {b} {bℓ}) _≈_
+≈-sym : ∀ {a b} → Sym (_≈_ {a} {b}) _≈_
 ≈-sym A≈B = record
   { f = A≈B.f⁻¹
   ; f⁻¹ = A≈B.f
-  ; cong₁ = A≈B.cong₂
-  ; cong₂ = A≈B.cong₁
   }
   where
   module A≈B = _≈_ A≈B
 
-≈-trans : ∀ {a aℓ b bℓ c cℓ} → Trans (_≈_ {a} {aℓ}) (_≈_ {b} {bℓ} {c} {cℓ}) _≈_
+≈-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⁻¹
-  ; cong₁ = B≈C.cong₁ ∘ A≈B.cong₁
-  ; cong₂ = A≈B.cong₂ ∘ B≈C.cong₂
   }
   where
   module A≈B = _≈_ A≈B
   module B≈C = _≈_ B≈C
 
-≈-isEquivalence : ∀ {a aℓ} → IsEquivalence (_≈_ {a} {aℓ} {a} {aℓ})
+≈-isEquivalence : ∀ {a} → IsEquivalence (_≈_ {a})
 ≈-isEquivalence = record
   { refl = ≈-refl
   ; sym = ≈-sym
   ; trans = ≈-trans
   }
 
-setoid : ∀ a aℓ → Setoid (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ)
-setoid a aℓ = record { isEquivalence = ≈-isEquivalence {a} {aℓ} }
+setoid : ∀ a → Setoid (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a)
+setoid a = record { isEquivalence = ≈-isEquivalence {a} }
 
-≤-refl : ∀ {a aℓ} → Reflexive (_≤_ {a} {aℓ})
+≤-refl : ∀ {a} → Reflexive (_≤_ {a})
 ≤-refl = record
   { f = id
-  ; cong = id
   }
 
-≤-reflexive : ∀ {a aℓ b bℓ} → _≈_ {a} {aℓ} {b} {bℓ} ⇒ _≤_
+≤-reflexive : ∀ {a b} → _≈_ {a} {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ℓ} → Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_
+≤-trans : ∀ {a b c} → Trans (_≤_ {a}) (_≤_ {b} {c}) _≤_
 ≤-trans A≤B B≤C = record
   { f = B≤C.f ∘ A≤B.f
-  ; cong = B≤C.cong ∘ A≤B.cong
   }
   where
   module A≤B = _≤_ A≤B
   module B≤C = _≤_ B≤C
 
-≤-antisym : ∀ {a aℓ b bℓ} → Antisym (_≤_ {a} {aℓ} {b} {bℓ}) _≤_ _≈_
+≤-antisym : ∀ {a b} → Antisym (_≤_ {a} {b}) _≤_ _≈_
 ≤-antisym A≤B B≤A = record
   { f = A≤B.f
   ; f⁻¹ = B≤A.f
-  ; cong₁ = A≤B.cong
-  ; cong₂ = B≤A.cong
   }
   where
   module A≤B = _≤_ A≤B
   module B≤A = _≤_ B≤A
 
-≤-min : ∀ {b bℓ} → Min (_≤_ {b = b} {bℓ}) ∅
+≤-min : ∀ {b} → Min (_≤_ {b = b}) ∅
 ≤-min A = record
   { f = λ ()
-  ; cong = λ {_} {_} {}
   }
 
-≤-isPartialOrder : ∀ a aℓ → IsPartialOrder (_≈_ {a} {aℓ}) _≤_
-≤-isPartialOrder a aℓ = record
+≤-isPartialOrder : ∀ a → IsPartialOrder (_≈_ {a}) _≤_
+≤-isPartialOrder a = record
   { isPreorder = record
     { isEquivalence = ≈-isEquivalence
     ; reflexive = ≤-reflexive
@@ -104,5 +92,5 @@ setoid a aℓ = record { isEquivalence = ≈-isEquivalence {a} {aℓ} }
   ; antisym = ≤-antisym
   }
 
-poset : ∀ a aℓ → Poset (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ) (c ⊔ a ⊔ aℓ)
-poset a aℓ = record { isPartialOrder = ≤-isPartialOrder a aℓ }
+poset : ∀ a → Poset (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) (c ⊔ a)
+poset a = record { isPartialOrder = ≤-isPartialOrder a }