Complete proofs up to Proposition 3.2 (excluding unrolling)

10 files changed, 596 insertions, 333 deletions

diff --git a/src/Cfe/Expression/Base.agda b/src/Cfe/Expression/Base.agda
index 4c53638..c4940b6 100644
--- a/src/Cfe/Expression/Base.agda
+++ b/src/Cfe/Expression/Base.agda
@@ -1,37 +1,69 @@
 {-# OPTIONS --without-K --safe #-}
 
+open import Function
 open import Relation.Binary
+import Relation.Binary.PropositionalEquality as ≡
 
 module Cfe.Expression.Base
-  {a ℓ} (setoid : Setoid a ℓ)
+  {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid setoid renaming (Carrier to A)
+open Setoid over renaming (Carrier to C)
 
-open import Cfe.Language setoid renaming (_∙_ to _∙ₗ_)
-open import Data.Fin hiding (_≤_)
-open import Data.Nat hiding (_≤_; _⊔_)
+open import Cfe.Language over as 𝕃
+open import Cfe.Language.Construct.Concatenate over renaming (_∙_ to _∙ₗ_)
+open import Cfe.Language.Construct.Single over
+open import Cfe.Language.Construct.Union over
+open import Cfe.Language.Indexed.Construct.Iterate over
+open import Data.Fin as F hiding (_≤_)
+open import Data.Nat as ℕ hiding (_≤_; _⊔_)
 open import Data.Product
 open import Data.Vec
-open import Level renaming (suc to lsuc)
-
-data Expression : ℕ → Set a where
-  ⊥ : {n : ℕ} → Expression n
-  ε : {n : ℕ} → Expression n
-  Char : {n : ℕ} → A → Expression n
-  _∨_ : {n : ℕ} → Expression n → Expression n → Expression n
-  _∙_ : {n : ℕ} → Expression n → Expression n → Expression n
-  Var : {n : ℕ} → Fin n → Expression n
-  μ : {n : ℕ} → Expression (suc n) → Expression n
-
-〚_〛 : {n : ℕ} → Expression n → Vec Language n → Language
-〚 ⊥ 〛 _ = ∅
-〚 ε 〛 _ = ｛ε｝
-〚 Char c 〛 _ = ｛ c ｝
-〚 e₁ ∨ e₂ 〛 γ = 〚 e₁ 〛 γ ∪ 〚 e₂ 〛 γ
-〚 e₁ ∙ e₂ 〛 γ = 〚 e₁ 〛 γ ∙ₗ 〚 e₂ 〛 γ
-〚 Var n 〛 γ = lookup γ n
-〚 μ e 〛 γ = fix (λ X → 〚 e 〛 (X ∷ γ))
-
-_≋_ : {n : ℕ} → Expression n → Expression n → Set (lsuc a ⊔ lsuc ℓ)
-e₁ ≋ e₂ = ∀ γ → 〚 e₁ 〛 γ ≤ 〚 e₂ 〛 γ × 〚 e₂ 〛 γ ≤ 〚 e₁ 〛 γ
+open import Level renaming (suc to lsuc) hiding (Lift)
+open import Relation.Nullary
+
+infix 10 _[_/_]
+infix 7 _∙_
+infix 6 _∨_
+infix 4 _≋_
+
+data Expression : ℕ → Set c where
+  ⊥ : ∀ {n} → Expression n
+  ε : ∀ {n} → Expression n
+  Char : ∀ {n} → C → Expression n
+  _∨_ : ∀ {n} → Expression n → Expression n → Expression n
+  _∙_ : ∀ {n} → Expression n → Expression n → Expression n
+  Var : ∀ {n} → Fin n → Expression n
+  μ : ∀ {n} → Expression (suc n) → Expression n
+
+wkn : ∀ {n} → Expression n → Fin (suc n) → Expression (suc n)
+wkn ⊥ i = ⊥
+wkn ε i = ε
+wkn (Char x) i = Char x
+wkn (e₁ ∨ e₂) i = wkn e₁ i ∨ wkn e₂ i
+wkn (e₁ ∙ e₂) i = wkn e₁ i ∙ wkn e₂ i
+wkn (Var x) i = Var (punchIn i x)
+wkn (μ e) i = μ (wkn e (suc i))
+
+_[_/_] : ∀ {n} → Expression (suc n) → Expression n → Fin (suc n) → Expression n
+⊥ [ e′ / i ] = ⊥
+ε [ e′ / i ] = ε
+Char x [ e′ / i ] = Char x
+(e₁ ∨ e₂) [ e′ / i ] = e₁ [ e′ / i ] ∨ e₂ [ e′ / i ]
+(e₁ ∙ e₂) [ e′ / i ] = e₁ [ e′ / i ] ∙ e₂ [ e′ / i ]
+Var j [ e′ / i ] with i F.≟ j
+... | yes i≡j = e′
+... | 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 ｝
+⟦ e₁ ∨ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∪ ⟦ e₂ ⟧ γ
+⟦ e₁ ∙ e₂ ⟧ γ = ⟦ e₁ ⟧ γ ∙ₗ ⟦ e₂ ⟧ γ
+⟦ Var n ⟧ γ = lookup γ n
+⟦ μ e ⟧ γ = ⋃ (λ X → ⟦ e ⟧ (X ∷ γ))
+
+_≋_ : {n : ℕ} → Expression n → Expression n → Set (lsuc (c ⊔ ℓ))
+e₁ ≋ e₂ = ∀ γ → ⟦ e₁ ⟧ γ 𝕃.≈ ⟦ e₂ ⟧ γ
diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
new file mode 100644
index 0000000..8bdc635
--- /dev/null
+++ b/src/Cfe/Expression/Properties.agda
@@ -0,0 +1,210 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Cfe.Expression.Properties
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+open Setoid over using () renaming (Carrier to C)
+
+open import Algebra
+open import Cfe.Expression.Base over
+open import Cfe.Language.Base over as L
+import Cfe.Language.Construct.Concatenate over as ∙
+import Cfe.Language.Construct.Union over as ∪
+import Cfe.Language.Indexed.Construct.Iterate over as ⋃
+open import Data.Fin as F
+open import Data.Nat as ℕ hiding (_⊔_)
+open import Data.Product
+open import Data.Sum
+open import Data.Unit
+open import Data.Vec
+open import Data.Vec.Properties
+import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+open import Function
+open import Level renaming (suc to lsuc)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
+open import Relation.Nullary
+
+isEquivalence : ∀ n → IsEquivalence (_≋_ {n})
+isEquivalence n = record
+  { refl = λ γ → ≈-refl
+  ; sym = λ x≋y γ → ≈-sym (x≋y γ)
+  ; trans = λ x≋y y≋z γ → ≈-trans (x≋y γ) (y≋z γ)
+  }
+
+isSemiring : ∀ n → IsSemiring (_≋_ {n}) _∨_ _∙_ ⊥ ε
+isSemiring n = record
+  { isSemiringWithoutAnnihilatingZero = record
+    { +-isCommutativeMonoid = record
+      { isMonoid = record
+        { isSemigroup = record
+          { isMagma = record
+            { isEquivalence = isEquivalence n
+            ; ∙-cong = λ x≋y u≋v γ → ∪-comm.∙-cong (x≋y γ) (u≋v γ)
+            }
+          ; assoc = λ x y z γ → ∪-comm.assoc (⟦ x ⟧ γ) (⟦ y ⟧ γ) (⟦ z ⟧ γ)
+          }
+        ; identity = (λ x γ → ∪-comm.identityˡ (⟦ x ⟧ γ)) , (λ x γ → ∪-comm.identityʳ (⟦ x ⟧ γ))
+        }
+      ; comm = λ x y γ → ∪-comm.comm (⟦ x ⟧ γ) (⟦ y ⟧ γ)
+      }
+    ; *-isMonoid = record
+      { isSemigroup = record
+        { isMagma = record
+          { isEquivalence = isEquivalence n
+          ; ∙-cong = λ x≋y u≋v γ → ∙-mon.∙-cong (x≋y γ) (u≋v γ)
+          }
+        ; assoc = λ x y z γ → ∙-mon.assoc (⟦ x ⟧ γ) (⟦ y ⟧ γ) (⟦ z ⟧ γ)
+        }
+      ; identity = (λ x γ → ∙-mon.identityˡ (⟦ x ⟧ γ)) , (λ x γ → ∙-mon.identityʳ (⟦ x ⟧ γ))
+      }
+    ; distrib = (λ x y z γ → record
+      { f = λ
+        { (l₁ , l₁∈⟦x⟧ , l₂ , inj₁ l₂∈⟦y⟧ , l₁++l₂≡l) → inj₁ (-, l₁∈⟦x⟧ , -, l₂∈⟦y⟧ , l₁++l₂≡l)
+        ; (l₁ , l₁∈⟦x⟧ , l₂ , inj₂ l₂∈⟦z⟧ , l₁++l₂≡l) → inj₂ (-, l₁∈⟦x⟧ , -, l₂∈⟦z⟧ , l₁++l₂≡l)
+        }
+      ; f⁻¹ = λ
+        { (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)
+        ; (l₁ , inj₂ l₁∈⟦z⟧ , l₂ , l₂∈⟦x⟧ , l₁++l₂≡l) → inj₂ (-, l₁∈⟦z⟧ , -, l₂∈⟦x⟧ , l₁++l₂≡l)
+        }
+      ; f⁻¹ = λ
+        { (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 _ where
+  open import Data.Vec.Relation.Binary.Equality.Setoid (L.setoid (c ⊔ ℓ) (c ⊔ ℓ)) as VE
+  open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
+
+  cong-env : ∀ {n} → (e : Expression n) → ∀ {γ γ′} → γ VE.≋ γ′ → ⟦ e ⟧ γ ≈ ⟦ e ⟧ γ′
+  cong-env ⊥ γ≈γ′ = ≈-refl
+  cong-env ε γ≈γ′ = ≈-refl
+  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)
+  cong-env (e₁ ∙ e₂) γ≈γ′ = ∙-cong (cong-env e₁ γ≈γ′) (cong-env e₂ γ≈γ′)
+    where
+    open IsMonoid (∙.isMonoid {c ⊔ ℓ} {c ⊔ ℓ})
+  cong-env (Var j) γ≈γ′ = PW.lookup γ≈γ′ j
+  cong-env (μ e) γ≈γ′ = ⋃.⋃-cong (λ x → cong-env e (x PW.∷ γ≈γ′))
+
+wkn-no-use : ∀ {n} → (e : Expression n) → ∀ i γ → ⟦ wkn e i ⟧ γ ≈ ⟦ e ⟧ (remove γ i)
+wkn-no-use ⊥ i γ = ≈-refl
+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)
+wkn-no-use (e₁ ∙ e₂) i γ = ∙-cong (wkn-no-use e₁ i γ) (wkn-no-use e₂ i γ)
+  where
+  open IsMonoid (∙.isMonoid {c ⊔ ℓ} {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 ≡.≡-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) ⟩
+  ⟦ wkn e (suc i) ⟧ (y ∷ z ∷ γ)      ≈⟨ wkn-no-use e (suc i) (y ∷ z ∷ γ) ⟩
+  ⟦ 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
+
+subst-fun : ∀ {n} → (e : Expression (suc n)) → ∀ e′ i γ → ⟦ e [ e′ / i ] ⟧ γ ≈ ⟦ e ⟧ (insert γ i (⟦ e′ ⟧ γ))
+subst-fun ⊥ e′ i γ = ≈-refl
+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)
+subst-fun (e₁ ∙ e₂) e′ i γ = ∙-cong (subst-fun e₁ e′ i γ) (subst-fun e₂ e′ i γ)
+  where
+  open IsMonoid (∙.isMonoid {c ⊔ ℓ} {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 ⊔ ℓ})
+... | 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 ⊔ ℓ})
+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
+
+  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′ 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
+
+unroll : ∀ {n} → (e : Expression (suc n)) → μ e ≋ e [ μ e / F.zero ]
+unroll e γ = begin
+  ⟦ μ e ⟧ γ ≈⟨ {!!} ⟩
+  (λ X → ⟦ e ⟧ (X ∷ γ)) (⟦ μ e ⟧ γ) ≡⟨⟩
+  ⟦ e ⟧ (⟦ μ e ⟧ γ ∷ γ) ≡⟨⟩
+  ⟦ e ⟧ (insert γ F.zero (⟦ μ e ⟧ γ)) ≈˘⟨ subst-fun e (μ e) F.zero γ ⟩
+  ⟦ e [ μ e / F.zero ] ⟧ γ ∎
+  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
+
+monotone : ∀ {n} (e : Expression n) → ⟦ e ⟧ Preserves PW.Pointwise L._≤_ ⟶ L._≤_
+monotone ⊥ γ≤γ′ = ≤-refl
+monotone ε γ≤γ′ = ≤-refl
+monotone (Char x) γ≤γ′ = ≤-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.∷ γ≤γ′))
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}
diff --git a/src/Relation/Binary/Construct/InducedPoset.agda b/src/Relation/Binary/Construct/InducedPoset.agda
deleted file mode 100644
index 30363e6..0000000
--- a/src/Relation/Binary/Construct/InducedPoset.agda
+++ /dev/null
@@ -1,70 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Relation.Binary
-
-module Relation.Binary.Construct.InducedPoset
-  {a ℓ} {A : Set a}
-  (_≤_ : Rel A ℓ)
-  where
-
-open import Algebra
-open import Data.Product
-open import Function
-open import Level
-
-_≈_ : Rel A ℓ
-_≈_ = _≤_ -×- flip _≤_
-
-AntiCongruent₁ : Op₁ A → Set (a ⊔ ℓ)
-AntiCongruent₁ f = f Preserves _≤_ ⟶ flip _≤_
-
-AntiCongruent₂ : Op₂ A → Set (a ⊔ ℓ)
-AntiCongruent₂ ∙ = ∙ Preserves₂ _≤_ ⟶ _≤_ ⟶ flip _≤_
-
-LeftAntiCongruent : Op₂ A → Set (a ⊔ ℓ)
-LeftAntiCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≤_ ⟶ flip _≤_
-
-RightAntiCongruent : Op₂ A → Set (a ⊔ ℓ)
-RightAntiCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≤_ ⟶ flip _≤_
-
-InducedPoset : Reflexive _≤_ → Transitive _≤_ → Poset a ℓ ℓ
-InducedPoset ≤-refl ≤-trans = record
-  { _≈_ = _≈_
-  ; _≤_ = _≤_
-  ; isPartialOrder = record
-    { isPreorder = record
-      { isEquivalence = record
-        { refl = ≤-refl , ≤-refl
-        ; sym = swap
-        ; trans = zip ≤-trans (flip ≤-trans)
-        }
-      ; reflexive = proj₁
-      ; trans = ≤-trans
-      }
-    ; antisym = _,_
-    }
-  }
-
-≤-cong→≈-cong : {f : Op₁ A} → Congruent₁ _≤_ f → Congruent₁ _≈_ f
-≤-cong→≈-cong ≤-cong = map ≤-cong ≤-cong
-
-≤-anticong→≈-cong : {f : Op₁ A} → AntiCongruent₁ f → Congruent₁ _≈_ f
-≤-anticong→≈-cong ≤-anticong = swap ∘ map ≤-anticong ≤-anticong
-
-≤-cong₂→≈-cong₂ : {∙ : Op₂ A} → Congruent₂ _≤_ ∙ → Congruent₂ _≈_ ∙
-≤-cong₂→≈-cong₂ ≤-cong₂ = zip ≤-cong₂ ≤-cong₂
-
-≤-anticong₂→≈-cong₂ : {∙ : Op₂ A} → AntiCongruent₂ ∙ → Congruent₂ _≈_ ∙
-≤-anticong₂→≈-cong₂ ≤-anticong₂ = swap ∘₂ zip ≤-anticong₂ ≤-anticong₂
-
-≤-congₗ→≈-congₗ : {∙ : Op₂ A} → LeftCongruent _≤_ ∙ → LeftCongruent _≈_ ∙
-≤-congₗ→≈-congₗ ≤-congₗ = map ≤-congₗ ≤-congₗ
-
-≤-anticongₗ→≈-congₗ : {∙ : Op₂ A} → LeftAntiCongruent ∙ → LeftCongruent _≈_ ∙
-≤-anticongₗ→≈-congₗ ≤-anticongₗ = swap ∘ map ≤-anticongₗ ≤-anticongₗ
-
-≤-congᵣ→≈-congᵣ : {∙ : Op₂ A} → RightCongruent _≤_ ∙ → RightCongruent _≈_ ∙
-≤-congᵣ→≈-congᵣ ≤-congᵣ = map ≤-congᵣ ≤-congᵣ
-
-≤-anticongᵣ→≈-congᵣ : {∙ : Op₂ A} → RightAntiCongruent ∙ → RightCongruent _≈_ ∙
-≤-anticongᵣ→≈-congᵣ ≤-anticongᵣ = swap ∘ map ≤-anticongᵣ ≤-anticongᵣ