Change Language definition to respects instead of custom congruence.

13 files changed, 238 insertions, 360 deletions

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index f4a8dc0..2023a71 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -66,10 +66,21 @@ Var j [ e′ / i ] with i F.≟ j
 ... | no i≢j = Var (punchOut i≢j)
 μ e [ e′ / i ] = μ (e [ wkn e′ F.zero / suc i ])
 
-⟦_⟧ : ∀ {n : ℕ} → Expression n → Vec (Language (c ⊔ ℓ) (c ⊔ ℓ)) n → Language (c ⊔ ℓ) (c ⊔ ℓ)
-⟦ ⊥ ⟧ _ = Lift (c ⊔ ℓ) (c ⊔ ℓ) ∅
-⟦ ε ⟧ _ = Lift ℓ (c ⊔ ℓ) ｛ε｝
-⟦ Char x ⟧ _ = Lift ℓ (c ⊔ ℓ) ｛ x ｝
+shift : ∀ {n} → Expression n → (i j : Fin n) → .(_ : i F.≤ j) → Expression n
+shift ⊥ _ _ _ = ⊥
+shift ε _ _ _ = ε
+shift (Char x) _ _ _ = Char x
+shift (e₁ ∨ e₂) i j i≤j = shift e₁ i j i≤j ∨ shift e₂ i j i≤j
+shift (e₁ ∙ e₂) i j i≤j = shift e₁ i j i≤j ∙ shift e₂ i j i≤j
+shift {suc n} (Var k) i j _ with i F.≟ k
+... | yes i≡k = Var j
+... | no i≢k = Var (punchIn j (punchOut i≢k))
+shift (μ e) i j i≤j = μ (shift e (suc i) (suc j) (s≤s i≤j))
+
+⟦_⟧ : ∀ {n : ℕ} → Expression n → Vec (Language (c ⊔ ℓ)) n → Language (c ⊔ ℓ)
+⟦ ⊥ ⟧ _ = Lift (c ⊔ ℓ) ∅
+⟦ ε ⟧ _ = Lift ℓ ｛ε｝
+⟦ Char x ⟧ _ = Lift ℓ ｛ x ｝
 ⟦ e₁ ∨ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∪ ⟦ e₂ ⟧ γ
 ⟦ e₁ ∙ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∙ₗ ⟦ e₂ ⟧ γ
 ⟦ Var n ⟧ γ = lookup γ n
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index 1e41f42..0b1ae2c 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -70,14 +70,6 @@ isSemiring n = record
         { (inj₁ (l₁ , l₁∈⟦x⟧ , l₂ , l₂∈⟦y⟧ , l₁++l₂≡l)) → -, l₁∈⟦x⟧ , -, inj₁ l₂∈⟦y⟧ , l₁++l₂≡l
         ; (inj₂ (l₁ , l₁∈⟦x⟧ , l₂ , l₂∈⟦z⟧ , l₁++l₂≡l)) → -, l₁∈⟦x⟧ , -, inj₂ l₂∈⟦z⟧ , l₁++l₂≡l
         }
-      ; cong₁ = λ
-        { (l₁≈l₁′ , ∪.A≈A l₂≈l₂′) → ∪.A≈A (l₁≈l₁′ , l₂≈l₂′)
-        ; (l₁≈l₁′ , ∪.B≈B l₂≈l₂′) → ∪.B≈B (l₁≈l₁′ , l₂≈l₂′)
-        }
-      ; cong₂ = λ
-        { (∪.A≈A (l₁≈l₁′ , l₂≈l₂′)) → l₁≈l₁′ , ∪.A≈A l₂≈l₂′
-        ; (∪.B≈B (l₁≈l₁′ , l₂≈l₂′)) → l₁≈l₁′ , ∪.B≈B l₂≈l₂′
-        }
       }) , (λ x y z γ → record
       { f = λ
         { (l₁ , inj₁ l₁∈⟦y⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l) → inj₁ (-, l₁∈⟦y⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l)
@@ -87,34 +79,22 @@ isSemiring n = record
         { (inj₁ (l₁ , l₁∈⟦y⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l)) → -, inj₁ l₁∈⟦y⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l
         ; (inj₂ (l₁ , l₁∈⟦z⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l)) → -, inj₂ l₁∈⟦z⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l
         }
-      ; cong₁ = λ
-        { (∪.A≈A l₁≈l₁′ , l₂≈l₂′) → ∪.A≈A (l₁≈l₁′ , l₂≈l₂′)
-        ; (∪.B≈B l₁≈l₁′ , l₂≈l₂′) → ∪.B≈B (l₁≈l₁′ , l₂≈l₂′)
-        }
-      ; cong₂ = λ
-        { (∪.A≈A (l₁≈l₁′ , l₂≈l₂′)) → ∪.A≈A l₁≈l₁′ , l₂≈l₂′
-        ; (∪.B≈B (l₁≈l₁′ , l₂≈l₂′)) → ∪.B≈B l₁≈l₁′ , l₂≈l₂′
-        }
       })
     }
   ; zero = (λ x γ → record
     { f = λ ()
     ; f⁻¹ = λ ()
-    ; cong₁ = λ {_} {_} {l₁∈⟦⊥∙x⟧} → case l₁∈⟦⊥∙x⟧ of (λ ())
-    ; cong₂ = λ {_} {_} {l₁∈⟦⊥⟧} → case l₁∈⟦⊥⟧ of (λ ())
     }) , (λ x γ → record
     { f = λ ()
     ; f⁻¹ = λ ()
-    ; cong₁ = λ {_} {_} {l₁∈⟦x∙⊥⟧} → case l₁∈⟦x∙⊥⟧ of (λ ())
-    ; cong₂ = λ {_} {_} {l₁∈⟦⊥⟧} → case l₁∈⟦⊥⟧ of (λ ())
     })
   }
   where
-  module ∪-comm = IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ})
-  module ∙-mon = IsMonoid (∙.isMonoid {ℓ} {c ⊔ ℓ})
+  module ∪-comm = IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ})
+  module ∙-mon = IsMonoid (∙.isMonoid {ℓ})
 
 module _ where
-  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ)) as VE
   open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
 
   cong-env : ∀ {n} → (e : Expression n) → ∀ {γ γ′} → γ VE.≋ γ′ → ⟦ e ⟧ γ ≈ ⟦ e ⟧ γ′
@@ -123,10 +103,10 @@ module _ where
   cong-env (Char x) γ≈γ′ = ≈-refl
   cong-env (e₁ ∨ e₂) γ≈γ′ = ∪-cong (cong-env e₁ γ≈γ′) (cong-env e₂ γ≈γ′)
     where
-    open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
+    open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
   cong-env (e₁ ∙ e₂) γ≈γ′ = ∙-cong (cong-env e₁ γ≈γ′) (cong-env e₂ γ≈γ′)
     where
-    open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+    open IsMonoid (∙.isMonoid {c ⊔ ℓ})
   cong-env (Var j) γ≈γ′ = PW.lookup γ≈γ′ j
   cong-env (μ e) γ≈γ′ = ⋃.⋃-cong (λ x → cong-env e (x PW.∷ γ≈γ′))
 
@@ -136,16 +116,16 @@ wkn-no-use ε i γ = ≈-refl
 wkn-no-use (Char x) i γ = ≈-refl
 wkn-no-use (e₁ ∨ e₂) i γ = ∪-cong (wkn-no-use e₁ i γ) (wkn-no-use e₂ i γ)
   where
-  open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
+  open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
 wkn-no-use (e₁ ∙ e₂) i γ = ∙-cong (wkn-no-use e₁ i γ) (wkn-no-use e₂ i γ)
   where
-  open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+  open IsMonoid (∙.isMonoid {c ⊔ ℓ})
 wkn-no-use (Var j) i γ = reflexive (begin
   lookup γ (punchIn i j)                                    ≡˘⟨ ≡.cong (λ x → lookup x (punchIn i j)) (insert-remove γ i) ⟩
   lookup (insert (remove γ i) i (lookup γ i)) (punchIn i j) ≡⟨ insert-punchIn (remove γ i) i (lookup γ i) j ⟩
   lookup (remove γ i) j                                     ∎)
   where
-  open IsEquivalence (≈-isEquivalence {c ⊔ ℓ} {c ⊔ ℓ})
+  open IsEquivalence (≈-isEquivalence {c ⊔ ℓ})
   open ≡.≡-Reasoning
 wkn-no-use (μ e) i (z ∷ γ) = ⋃.⋃-cong (λ {x} {y} x≈y → begin
   ⟦ wkn e (suc i) ⟧ (x ∷ z ∷ γ)      ≈⟨ cong-env (wkn e (suc i)) (x≈y ∷ ≋-refl) ⟩
@@ -153,8 +133,8 @@ wkn-no-use (μ e) i (z ∷ γ) = ⋃.⋃-cong (λ {x} {y} x≈y → begin
   ⟦ e ⟧ (remove (y ∷ z ∷ γ) (suc i)) ≡⟨⟩
   ⟦ e ⟧ (y ∷ remove (z ∷ γ) i)       ∎)
   where
-  open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ))
-  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+  open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ))
+  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ)) as VE
 
 subst-fun : ∀ {n} → (e : Expression (suc n)) → ∀ e′ i γ → ⟦ e [ e′ / i ] ⟧ γ ≈ ⟦ e ⟧ (insert γ i (⟦ e′ ⟧ γ))
 subst-fun ⊥ e′ i γ = ≈-refl
@@ -162,42 +142,42 @@ subst-fun ε e′ i γ = ≈-refl
 subst-fun (Char x) e′ i γ = ≈-refl
 subst-fun {n} (e₁ ∨ e₂) e′ i γ = ∪-cong (subst-fun e₁ e′ i γ) (subst-fun e₂ e′ i γ)
   where
-  open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ} {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
+  open IsCommutativeMonoid (∪.isCommutativeMonoid {c ⊔ ℓ}) renaming (∙-cong to ∪-cong)
 subst-fun (e₁ ∙ e₂) e′ i γ = ∙-cong (subst-fun e₁ e′ i γ) (subst-fun e₂ e′ i γ)
   where
-  open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+  open IsMonoid (∙.isMonoid {c ⊔ ℓ})
 subst-fun (Var j) e′ i γ with i F.≟ j
 ... | yes _≡_.refl = sym (reflexive (insert-lookup γ i (⟦ e′ ⟧ γ)))
   where
-  open IsEquivalence (≈-isEquivalence {c ⊔ ℓ} {c ⊔ ℓ})
+  open IsEquivalence (≈-isEquivalence {c ⊔ ℓ})
 ... | no i≢j = reflexive (begin
                  lookup γ (punchOut i≢j) ≡˘⟨ ≡.cong (λ x → lookup x (punchOut i≢j)) (remove-insert γ i (⟦ e′ ⟧ γ)) ⟩
                  lookup (remove (insert γ i (⟦ e′ ⟧ γ)) i) (punchOut i≢j) ≡⟨ remove-punchOut (insert γ i (⟦ e′ ⟧ γ)) i≢j ⟩
                  lookup (insert γ i (⟦ e′ ⟧ γ)) j ∎)
   where
   open ≡.≡-Reasoning
-  open IsEquivalence (≈-isEquivalence {c ⊔ ℓ} {c ⊔ ℓ})
+  open IsEquivalence (≈-isEquivalence {c ⊔ ℓ})
 subst-fun (μ e) e′ i γ = ⋃.⋃-cong λ {x} {y} x≈y → begin
   ⟦ e [ wkn e′ F.zero / suc i ] ⟧ (x ∷ γ) ≈⟨ cong-env (e [ wkn e′ F.zero / suc i ]) (x≈y ∷ ≋-refl) ⟩
   ⟦ e [ wkn e′ F.zero / suc i ] ⟧ (y ∷ γ) ≈⟨ subst-fun e (wkn e′ F.zero) (suc i) (y ∷ γ) ⟩
   ⟦ e ⟧ (y ∷ insert γ i (⟦ wkn e′ F.zero ⟧ (y ∷ γ))) ≈⟨ cong-env e (≈-refl ∷ insert′ (wkn-no-use e′ F.zero (y ∷ γ)) ≋-refl i) ⟩
   ⟦ e ⟧ (y ∷ insert γ i (⟦ e′ ⟧ γ)) ∎
   where
-  open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ))
-  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+  open import Relation.Binary.Reasoning.Setoid (L.setoid (c ⊔ ℓ))
+  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ)) as VE
 
-  insert′ : ∀ {n x y} {xs ys : Vec (Language (c ⊔ ℓ) (c ⊔ ℓ)) n} → x ≈ y → xs VE.≋ ys → (i : Fin (suc n)) → insert xs i x VE.≋ insert ys i y
+  insert′ : ∀ {n x y} {xs ys : Vec (Language (c ⊔ ℓ)) n} → x ≈ y → xs VE.≋ ys → (i : Fin (suc n)) → insert xs i x VE.≋ insert ys i y
   insert′ x≈y xs≋ys F.zero = x≈y ∷ xs≋ys
   insert′ x≈y (z≈w ∷ xs≋ys) (suc i) = z≈w ∷ insert′ x≈y xs≋ys i
 
-monotone : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_
-monotone ⊥ γ≤γ′ = L.≤-refl
-monotone ε γ≤γ′ = L.≤-refl
-monotone (Char x) γ≤γ′ = L.≤-refl
-monotone (e₁ ∨ e₂) γ≤γ′ = ∪.∪-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
-monotone (e₁ ∙ e₂) γ≤γ′ = ∙.∙-monotone (monotone e₁ γ≤γ′) (monotone e₂ γ≤γ′)
-monotone (Var i) γ≤γ′ = PW.lookup γ≤γ′ i
-monotone (μ e) γ≤γ′ = ⋃.⋃-monotone (λ x≤y → monotone e (x≤y PW.∷ γ≤γ′))
+mono : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_
+mono ⊥ γ≤γ′ = L.≤-refl
+mono ε γ≤γ′ = L.≤-refl
+mono (Char x) γ≤γ′ = L.≤-refl
+mono (e₁ ∨ e₂) γ≤γ′ = ∪.∪-mono (mono e₁ γ≤γ′) (mono e₂ γ≤γ′)
+mono (e₁ ∙ e₂) γ≤γ′ = ∙.∙-mono (mono e₁ γ≤γ′) (mono e₂ γ≤γ′)
+mono (Var i) γ≤γ′ = PW.lookup γ≤γ′ i
+mono (μ e) γ≤γ′ = ⋃.⋃-mono (λ x≤y → mono e (x≤y PW.∷ γ≤γ′))
 
 cast-inverse : ∀ {m n} e → .(m≡n : m ≡ n) → .(n≡m : n ≡ m) → E.cast m≡n (E.cast n≡m e) ≡ e
 cast-inverse ⊥ m≡n n≡m = ≡.refl
diff --git a/src/Cfe/Judgement/Base.agda b/src/Cfe/Judgement/Base.agda
index 4623066..754d92d 100644
--- a/src/Cfe/Judgement/Base.agda
+++ b/src/Cfe/Judgement/Base.agda
@@ -28,10 +28,10 @@ data _,_⊢_∶_ : {m : ℕ} → {n : ℕ} → Vec (Type ℓ ℓ) m → Vec (Typ
   Vee : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e₁ e₂ τ₁ τ₂} → Γ , Δ ⊢ e₁ ∶ τ₁ → Γ , Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ , Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂
 
 vcast : ∀ {a A m n} → .(m ≡ n) → Vec {a} A m → Vec A n
+vcast {n = ℕ.zero} eq [] = []
 vcast {n = suc n} eq (x ∷ xs) = x ∷ vcast (suc-injective eq) xs
   where
   open import Data.Nat.Properties using (suc-injective)
-vcast {n = ℕ.zero} eq [] = []
 
 data _≅_ {a A} : {m n : ℕ} → Vec {a} A m → Vec A n → Set a where
   []≅[] : [] ≅ []
diff --git a/src/Cfe/Judgement/Properties.agda b/src/Cfe/Judgement/Properties.agda
index 101994b..1c06fcd 100644
--- a/src/Cfe/Judgement/Properties.agda
+++ b/src/Cfe/Judgement/Properties.agda
@@ -13,11 +13,65 @@ open import Data.Empty
 open import Data.Fin as F hiding (cast)
 open import Data.Fin.Properties
 open import Data.Nat as ℕ
-open import Data.Nat.Properties
+open import Data.Nat.Properties as NP
 open import Data.Vec
 open import Data.Vec.Properties
 open import Function
 open import Relation.Binary.PropositionalEquality
+open import Relation.Nullary
+
+private
+  raise-mono : ∀ {m n i j} → i F.≤ j → raise {n} m i F.≤ raise m j
+  raise-mono {zero} i≤j = i≤j
+  raise-mono {suc m} i≤j = s≤s (raise-mono i≤j)
+
+  raise≤ : ∀ {m} n i → n ℕ.≤ toℕ (raise {m} n i)
+  raise≤ zero i = z≤n
+  raise≤ (suc n) i = s≤s (raise≤ n i)
+
+  inject+≤raise : ∀ {m n} i j → inject+ {suc n} m i F.≤ F.cast (+-suc n m) (raise {suc m} n j)
+  inject+≤raise {m} {n} i j = begin
+    toℕ (inject+ m i)          ≡˘⟨ toℕ-inject+ m i ⟩
+    toℕ i                      ≤⟨ NP.<⇒≤pred (toℕ<n i) ⟩
+    n                          ≤⟨ m≤m+n n (toℕ j) ⟩
+    n ℕ.+ toℕ j                ≡˘⟨ toℕ-raise n j ⟩
+    toℕ (raise n j)            ≡˘⟨ toℕ-cast (+-suc n m) (raise n j) ⟩
+    toℕ (F.cast _ (raise n j)) ∎
+    where
+    open ≤-Reasoning
+
+  toℕ-punchIn : ∀ {m} i j → toℕ j ℕ.≤ toℕ (punchIn {m} i j)
+  toℕ-punchIn zero j = n≤1+n (toℕ j)
+  toℕ-punchIn (suc i) zero = z≤n
+  toℕ-punchIn (suc i) (suc j) = s≤s (toℕ-punchIn i j)
+
+  toℕ-punchOut : ∀ {m i j} → (i≢j : i ≢ j) → toℕ j ℕ.≤ suc (toℕ (punchOut {m} i≢j))
+  toℕ-punchOut {_} {zero} {zero} i≢j = ⊥-elim (i≢j refl)
+  toℕ-punchOut {_} {zero} {suc j} i≢j = NP.≤-refl
+  toℕ-punchOut {suc m} {suc i} {zero} i≢j = z≤n
+  toℕ-punchOut {suc m} {suc i} {suc j} i≢j = s≤s (toℕ-punchOut (i≢j ∘ cong suc))
+
+  toℕ-reduce : ∀ {m n} i i≥m → toℕ (reduce≥ {m} {n} i i≥m) ≡ toℕ i ∸ m
+  toℕ-reduce {zero} i i≥m = refl
+  toℕ-reduce {suc m} (suc i) (s≤s i≥m) = toℕ-reduce i i≥m
+
+  <⇒punchOut≤ : ∀ {m n i j} → n ℕ.< toℕ j → (i≢j : i ≢ j) → n ℕ.≤ toℕ (punchOut {m} i≢j)
+  <⇒punchOut≤ {m} {n} {zero} {suc j} (s≤s n<j) i≢j = n<j
+  <⇒punchOut≤ {suc m} {zero} {suc i} {suc j} (s≤s n<j) i≢j = z≤n
+  <⇒punchOut≤ {suc m} {suc n} {suc i} {suc j} (s≤s n<j) i≢j = s≤s (<⇒punchOut≤ n<j (i≢j ∘ cong suc))
+
+  punchIn-∸ : ∀ {m n} i {j} j≥n → toℕ (punchIn (F.cast (+-suc n m) (raise n i)) j) ∸ n ≡ toℕ (punchIn i (reduce≥ j j≥n))
+  punchIn-∸ {zero} {n} zero {j} j≥n = ⊥-elim (<⇒≱ (begin-strict
+    toℕ j ≡˘⟨ toℕ-cast (+-identityʳ n) j ⟩
+    toℕ (F.cast _ j) <⟨ toℕ<n (F.cast _ j) ⟩
+    n ∎) j≥n)
+    where
+    open ≤-Reasoning
+  punchIn-∸ {suc m} {zero} zero {j} z≤n = refl
+  punchIn-∸ {suc m} {suc n} zero {suc j} (s≤s j≥n) = punchIn-∸ zero j≥n
+  punchIn-∸ {suc m} {zero} (suc i) {zero} z≤n = refl
+  punchIn-∸ {suc m} {zero} (suc i) {suc j} z≤n = cong suc (punchIn-∸ i z≤n)
+  punchIn-∸ {suc m} {suc n} (suc i) {suc j} (s≤s j≥n) = punchIn-∸ (suc i) j≥n
 
 ≅-refl : ∀ {a A m} {xs : Vec {a} A m} → xs ≅ xs
 ≅-refl {xs = []} = []≅[]
@@ -30,6 +84,10 @@ open import Relation.Binary.PropositionalEquality
 ≅-length []≅[] = refl
 ≅-length (_ ∷ xs≅ys) = cong suc (≅-length xs≅ys)
 
+≅-vcast : ∀ {a A m n} {xs : Vec {a} A m} → .(m≡n : m ≡ n) → vcast m≡n xs ≅ xs
+≅-vcast {n = zero} {[]} m≡n = []≅[]
+≅-vcast {n = suc n} {x ∷ xs} m≡n = refl ∷ ≅-vcast (NP.suc-injective m≡n)
+
 ≅⇒≡ : ∀ {a A m n} {xs : Vec {a} A m} {ys : Vec _ n} → (xs≅ys : xs ≅ ys) → vcast (≅-length xs≅ys) xs ≡ ys
 ≅⇒≡ []≅[] = refl
 ≅⇒≡ (x≡y ∷ xs≅ys) = cong₂ _∷_ x≡y (≅⇒≡ xs≅ys)
@@ -69,7 +127,7 @@ cast₁ eq (Fix Γ₁,τ∷Δ⊢e∶τ) = Fix (cast₁ eq Γ₁,τ∷Δ⊢e∶τ
 cast₁ {Δ = Δ} eq (Cat Γ₁,Δ⊢e₁∶τ₁ Δ++Γ₁,∙⊢e₂∶τ₂ τ₁⊛τ₂) = Cat (cast₁ eq Γ₁,Δ⊢e₁∶τ₁) (cast₁ (++ˡ Δ eq) Δ++Γ₁,∙⊢e₂∶τ₂) τ₁⊛τ₂
 cast₁ eq (Vee Γ₁,Δ⊢e₁∶τ₁ Γ₁,Δ⊢e₂∶τ₂ τ₁#τ₂) = Vee (cast₁ eq Γ₁,Δ⊢e₁∶τ₁) (cast₁ eq Γ₁,Δ⊢e₂∶τ₂) τ₁#τ₂
 
-wkn₁ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
+wkn₁ : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e τ} →
        Γ , Δ ⊢ e ∶ τ →
        ∀ τ′ i →
        insert Γ i τ′ , Δ ⊢ cast (sym (+-suc n m)) (wkn e (F.cast (+-suc n m) (raise n i))) ∶ τ
@@ -78,16 +136,11 @@ wkn₁ (Char c) τ′ i = Char c
 wkn₁ Bot τ′ i = Bot
 wkn₁ {m} {n} {Γ} {Δ} {e} {τ} (Var {i = j} j≥n) τ′ i =
   subst (insert Γ i τ′ , Δ ⊢ cast (sym (+-suc n m)) (Var (punchIn (F.cast (+-suc n m) (raise n i)) j)) ∶_)
-        (eq Γ τ′ i j≥n)
-        (Var (le i j≥n))
+        eq
+        (Var le)
   where
-  toℕ-punchIn : ∀ {m} i j → toℕ j ℕ.≤ toℕ (punchIn {m} i j)
-  toℕ-punchIn zero j = n≤1+n (toℕ j)
-  toℕ-punchIn (suc i) zero = z≤n
-  toℕ-punchIn (suc i) (suc j) = s≤s (toℕ-punchIn i j)
-
-  le : ∀ {m n} i {j} → toℕ j ≥ n → toℕ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) ≥ n
-  le {m} {n} i {j} j≥n = begin
+  le : toℕ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) ≥ n
+  le  = begin
     n ≤⟨ j≥n ⟩
     toℕ j ≤⟨ toℕ-punchIn (F.cast (+-suc n m) (raise n i)) j ⟩
     toℕ (punchIn (F.cast _ (raise n i)) j) ≡˘⟨ toℕ-cast (sym (+-suc n m)) (punchIn (F.cast _ (raise n i)) j) ⟩
@@ -99,35 +152,18 @@ wkn₁ {m} {n} {Γ} {Δ} {e} {τ} (Var {i = j} j≥n) τ′ i =
   lookup-cast l zero = refl
   lookup-cast (x ∷ l) (suc j) = lookup-cast l j
 
-  toℕ-reduce : ∀ {m n} i i≥m → toℕ (reduce≥ {m} {n} i i≥m) ≡ toℕ i ∸ m
-  toℕ-reduce {zero} i i≥m = refl
-  toℕ-reduce {suc m} (suc i) (s≤s i≥m) = toℕ-reduce i i≥m
-
-  punchIn-∸ : ∀ {m n} i {j} j≥n → toℕ (punchIn (F.cast (+-suc n m) (raise n i)) j) ∸ n ≡ toℕ (punchIn i (reduce≥ j j≥n))
-  punchIn-∸ {zero} {n} zero {j} j≥n = ⊥-elim (<⇒≱ (begin-strict
-    toℕ j ≡˘⟨ toℕ-cast (+-identityʳ n) j ⟩
-    toℕ (F.cast _ j) <⟨ toℕ<n (F.cast _ j) ⟩
-    n ∎) j≥n)
-    where
-    open ≤-Reasoning
-  punchIn-∸ {suc m} {zero} zero {j} z≤n = refl
-  punchIn-∸ {suc m} {suc n} zero {suc j} (s≤s j≥n) = punchIn-∸ zero j≥n
-  punchIn-∸ {suc m} {zero} (suc i) {zero} z≤n = refl
-  punchIn-∸ {suc m} {zero} (suc i) {suc j} z≤n = cong suc (punchIn-∸ i z≤n)
-  punchIn-∸ {suc m} {suc n} (suc i) {suc j} (s≤s j≥n) = punchIn-∸ (suc i) j≥n
-
-  missing-link : ∀ {m n} i {j} j≥n → reduce≥ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) (le i j≥n) ≡ punchIn i (reduce≥ j j≥n)
-  missing-link {n = n} i {j} j≥n = toℕ-injective (begin
-    toℕ (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n)) ≡⟨ toℕ-reduce (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n) ⟩
+  missing-link : reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le ≡ punchIn i (reduce≥ j j≥n)
+  missing-link = toℕ-injective (begin
+    toℕ (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le) ≡⟨ toℕ-reduce (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le ⟩
     toℕ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) ∸ n ≡⟨ cong (_∸ n) (toℕ-cast _ (punchIn (F.cast _ (raise n i)) j)) ⟩
     toℕ (punchIn (F.cast _ (raise n i)) j) ∸ n ≡⟨ punchIn-∸ i j≥n ⟩
     toℕ (punchIn i (reduce≥ j j≥n)) ∎)
     where
     open ≡-Reasoning
 
-  eq : ∀ {a} {A : Set a} {m n} (Γ : Vec A m) τ′ i {j} j≥n → lookup (insert Γ i τ′) (reduce≥ (F.cast (sym (+-suc n m)) (punchIn (F.cast (+-suc n m) (raise n i)) j)) (le i {j} j≥n)) ≡ lookup Γ (reduce≥ j j≥n)
-  eq {n = n} Γ τ′ i {j} j≥n = begin
-    lookup (insert Γ i τ′) (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) (le i j≥n)) ≡⟨ cong (lookup (insert Γ i τ′)) (missing-link i j≥n) ⟩
+  eq : lookup (insert Γ i τ′) (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le) ≡ lookup Γ (reduce≥ j j≥n)
+  eq = begin
+    lookup (insert Γ i τ′) (reduce≥ (F.cast _ (punchIn (F.cast _ (raise n i)) j)) le) ≡⟨ cong (lookup (insert Γ i τ′)) missing-link ⟩
     lookup (insert Γ i τ′) (punchIn i (reduce≥ j j≥n)) ≡⟨ insert-punchIn Γ i τ′ (reduce≥ j j≥n) ⟩
     lookup Γ (reduce≥ j j≥n) ∎
     where
@@ -157,10 +193,9 @@ wkn₁{m} {n} {Γ} {Δ} (Cat {e₂ = e₂} {τ₂ = τ₂} Γ,Δ⊢e₁∶τ₁
     toℕ (F.cast k≡m i) ≡⟨ toℕ-cast k≡m i ⟩
     toℕ i ≡˘⟨ toℕ-cast k≡n i ⟩
     toℕ (F.cast k≡n i) ∎)
-
 wkn₁ (Vee Γ,Δ⊢e₁∶τ₁ Γ,Δ⊢e₂∶τ₂ τ₁#τ₂) τ′ i = Vee (wkn₁ Γ,Δ⊢e₁∶τ₁ τ′ i) (wkn₁ Γ,Δ⊢e₂∶τ₂ τ′ i) τ₁#τ₂
 
-wkn₂ : ∀ {m n} {Γ : Vec (Type ℓ ℓ) m} {Δ : Vec (Type ℓ ℓ) n} {e τ} →
+wkn₂ : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e τ} →
        Γ , Δ ⊢ e ∶ τ →
        ∀ τ′ i →
        Γ , insert Δ i τ′ ⊢ wkn e (inject+ m i) ∶ τ
@@ -177,13 +212,10 @@ wkn₂ {m} {n} {Γ} {Δ} (Var {i = j} j≥n) τ′ i =
   where
   open ≤-Reasoning
 
-  m<n+1⇒m≤n : ∀ {m n} → m ℕ.< suc n → m ℕ.≤ n
-  m<n+1⇒m≤n (s≤s m≤n) = m≤n
-
   i≤j : toℕ (inject+ m i) ℕ.≤ toℕ j
   i≤j = begin
     toℕ (inject+ m i) ≡˘⟨ toℕ-inject+ m i ⟩
-    toℕ i ≤⟨ m<n+1⇒m≤n (toℕ<n i) ⟩
+    toℕ i ≤⟨ NP.<⇒≤pred (toℕ<n i) ⟩
     n ≤⟨ j≥n ⟩
     toℕ j ∎
 
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 }
diff --git a/src/Cfe/Type/Base.agda b/src/Cfe/Type/Base.agda
index 371bc2f..a5ed780 100644
--- a/src/Cfe/Type/Base.agda
+++ b/src/Cfe/Type/Base.agda
@@ -48,7 +48,7 @@ _∙_ {lℓ₁ = lℓ₁} {fℓ₂} {lℓ₂} τ₁ τ₂ = record
   ; Flast = Flast τ₂ ∪ (if Null τ₂ then First τ₂ ∪ Flast τ₁ else λ x → L.Lift (lℓ₁ ⊔ fℓ₂) (x U.∈ U.∅))
   }
 
-record _⊨_ {a} {aℓ} {fℓ} {lℓ} (A : Language a aℓ) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
+record _⊨_ {a} {fℓ} {lℓ} (A : Language a) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
   field
     n⇒n : null A → T (Null τ)
     f⇒f : first A ⊆ First τ
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 2222fbe..cfdf694 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -13,10 +13,11 @@ open import Cfe.Language.Construct.Single over
 open import Cfe.Type.Base over
 open import Data.Empty
 open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Product
 open import Function
 
-⊨-anticongˡ : ∀ {a aℓ b bℓ fℓ lℓ} {A : Language a aℓ} {B : Language b bℓ} {τ : Type fℓ lℓ} → B ≤ A → A ⊨ τ → B ⊨ τ
+⊨-anticongˡ : ∀ {a b fℓ lℓ} {A : Language a} {B : Language b} {τ : Type fℓ lℓ} → B ≤ A → A ⊨ τ → B ⊨ τ
 ⊨-anticongˡ B≤A A⊨τ = record
   { n⇒n = A⊨τ.n⇒n ∘ B≤A.f
   ; f⇒f = A⊨τ.f⇒f ∘ map₂ B≤A.f
@@ -26,12 +27,10 @@ open import Function
   module B≤A = _≤_ B≤A
   module A⊨τ = _⊨_ A⊨τ
 
-L⊨τ⊥⇒L≈∅ : ∀ {a aℓ} {L : Language a aℓ} → L ⊨ τ⊥ → L ≈ ∅
+L⊨τ⊥⇒L≈∅ : ∀ {a} {L : Language a} → L ⊨ τ⊥ → L ≈ ∅
 L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   { f = λ {l} → elim l
   ; f⁻¹ = λ ()
-  ; cong₁ = λ {l} {_} {l∈L} → ⊥-elim (elim l l∈L)
-  ; cong₂ = λ {_} {_} {}
   }
   where
   module L⊨τ⊥ = _⊨_ L⊨τ⊥
@@ -47,10 +46,9 @@ L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   ; l⇒l = λ ()
   }
 
-L⊨τε⇒L≤｛ε｝ : ∀ {a aℓ} {L : Language a aℓ} → L ⊨ τε → L ≤ ｛ε｝
+L⊨τε⇒L≤｛ε｝ : ∀ {a} {L : Language a} → L ⊨ τε → L ≤ ｛ε｝
 L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
   { f = λ {l} → elim l
-  ; cong = const tt
   }
   where
   open import Data.Unit
@@ -73,16 +71,12 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
 ｛c｝⊨τ[c] : ∀ c → ｛ c ｝ ⊨ τ[ c ]
 ｛c｝⊨τ[c] c = record
   { n⇒n = λ ()
-  ; f⇒f = λ {x} → λ {([] , (a , eq , a∼c)) → begin
-    c ≈˘⟨ a∼c ⟩
-    a ≡˘⟨ proj₁ (∷-injective eq) ⟩
-    x ∎}
-  ; l⇒l = λ
+  ; f⇒f = λ {x} → λ {([] , (c∼x ∷ []≋[])) → c∼x}
+  ; l⇒l = λ {x} → λ
     { ([] , []≢[] , _) → ⊥-elim ([]≢[] refl)
-    ; (x ∷ [] , x∷[]≢[] , ())
+    ; (y ∷ [] , _ , l′ , y∷x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y x l′ y∷x∷l′∈｛c｝)
+    ; (y ∷ z ∷ l , _ , l′ , y∷z∷l++x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y z (l ++ x ∷ l′) y∷z∷l++x∷l′∈｛c｝)
     }
   }
   where
-  open import Data.List.Properties
-  open import Relation.Binary.Reasoning.Setoid over
   open import Relation.Binary.PropositionalEquality