Another redefinition of Language.

6 files changed, 329 insertions, 242 deletions

diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index c1ff398..f0d1bb7 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -1,118 +1,163 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary
+open import Relation.Binary as B using (Setoid)
 
 module Cfe.Language.Base
-  {c ℓ} (setoid : Setoid c ℓ)
+  {c ℓ} (over : Setoid c ℓ)
   where
 
-open Setoid setoid renaming (Carrier to A)
+open Setoid over using () renaming (Carrier to C)
 
+open import Cfe.Relation.Indexed
 open import Data.Empty
 open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid setoid
-open import Data.Product as Product
-open import Function
-open import Level
+open import Data.List.Relation.Binary.Equality.Setoid over
+open import Data.Product
+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 ≡
-import Relation.Binary.Indexed.Heterogeneous as I
+open import Relation.Binary.Indexed.Heterogeneous
 
-record IsLanguage {a aℓ} (𝕃 : List A → Set a) (_≈ᴸ_ : ∀ {l} → Rel (𝕃 l) aℓ) (⤖ : ∀ {l₁ l₂} → l₁ ≋ l₂ → 𝕃 l₁ → 𝕃 l₂) : Set (c ⊔ ℓ ⊔ a ⊔ aℓ) where
-  field
-    ≈ᴸ-isEquivalence : ∀ {l} → IsEquivalence (_≈ᴸ_ {l})
-    ⤖-cong : ∀ {l₁ l₂ l₁≋l₂} → (⤖ l₁≋l₂) Preserves _≈ᴸ_ {l₁} ⟶ _≈ᴸ_ {l₂}
-    ⤖-bijective : ∀ {l₁ l₂ l₁≋l₂} → Bijective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ l₁≋l₂)
-    ⤖-refl : ∀ {l l∈𝕃} → (⤖ {l} ≋-refl l∈𝕃) ≈ᴸ l∈𝕃
-    ⤖-sym : ∀ {l₁ l₂ l₁∈𝕃 l₂∈𝕃 l₁≋l₂}
-          → (⤖ {l₁} l₁≋l₂ l₁∈𝕃) ≈ᴸ l₂∈𝕃
-          → (⤖ {l₂} (≋-sym l₁≋l₂) l₂∈𝕃) ≈ᴸ l₁∈𝕃
-    ⤖-trans : ∀ {l₁ 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₃∈𝕃
-
-  ≈ᴸ-refl : ∀ {l} → Reflexive (_≈ᴸ_ {l})
-  ≈ᴸ-refl = IsEquivalence.refl ≈ᴸ-isEquivalence
-
-  ≈ᴸ-sym : ∀ {l} → Symmetric (_≈ᴸ_ {l})
-  ≈ᴸ-sym = IsEquivalence.sym ≈ᴸ-isEquivalence
-
-  ≈ᴸ-trans : ∀ {l} → Transitive (_≈ᴸ_ {l})
-  ≈ᴸ-trans = IsEquivalence.trans ≈ᴸ-isEquivalence
-
-  ≈ᴸ-reflexive : ∀ {l} → ≡._≡_ ⇒ (_≈ᴸ_ {l})
-  ≈ᴸ-reflexive = IsEquivalence.reflexive ≈ᴸ-isEquivalence
-
-  ⤖-injective : ∀ {l₁ l₂ l₁≋l₂} → Injective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ l₁≋l₂)
-  ⤖-injective = proj₁ ⤖-bijective
-
-  ⤖-surjective : ∀ {l₁ l₂ l₁≋l₂} → Surjective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ {l₁} l₁≋l₂)
-  ⤖-surjective = proj₂ ⤖-bijective
-
-  ⤖-isIndexedEquivalence : I.IsIndexedEquivalence 𝕃 (λ l₁∈𝕃 l₂∈𝕃 → ∃[ l₁≋l₂ ] ((⤖ l₁≋l₂ l₁∈𝕃) ≈ᴸ l₂∈𝕃))
-  ⤖-isIndexedEquivalence = record
-    { refl = ≋-refl , ⤖-refl
-    ; sym = Product.map ≋-sym ⤖-sym
-    ; trans = Product.zip ≋-trans ⤖-trans
+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 ⊔ ℓ)
+｛ε｝ = record
+  { Carrier = [] ≋_
+  ; _≈_ = λ {l₁} {l₂} []≋l₁ []≋l₂ → ∃[ l₁≋l₂ ] (≋-trans []≋l₁ l₁≋l₂ ≡.≡ []≋l₂)
+  ; 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} )
     }
+  }
 
-  ⤖-reflexive : ∀ {l l∈𝕃 l∈𝕃′} → l∈𝕃 ≡.≡ l∈𝕃′ → ∃[ l≋l ]((⤖ {l} l≋l l∈𝕃) ≈ᴸ l∈𝕃′)
-  ⤖-reflexive = I.IsIndexedEquivalence.reflexive ⤖-isIndexedEquivalence
+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)
+    }
+  }
+  where
+  module A = IndexedSetoid A
 
-record Language a aℓ : Set (c ⊔ ℓ ⊔ suc (a ⊔ aℓ)) where
-  infix 4 _≈ᴸ_
-  field
-    𝕃 : List A → Set a
-    _≈ᴸ_ : ∀ {l} → Rel (𝕃 l) aℓ
-    ⤖ : ∀ {l₁ l₂} → l₁ ≋ l₂ → 𝕃 l₁ → 𝕃 l₂
-    isLanguage : IsLanguage 𝕃 _≈ᴸ_ ⤖
+𝕃 : ∀ {a aℓ} → Language a aℓ → List C → Set a
+𝕃 = IndexedSetoid.Carrier
 
-  open IsLanguage isLanguage public
+_∈_ : ∀ {a aℓ} → List C → Language a aℓ → Set a
+_∈_ = flip 𝕃
 
-open Language
+≈ᴸ : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → 𝕃 A l₁ → 𝕃 A l₂ → Set aℓ
+≈ᴸ = IndexedSetoid._≈_
 
-infix 4 _∈_
+≈ᴸ-refl : ∀ {a aℓ} → (A : Language a aℓ) → Reflexive (𝕃 A) (≈ᴸ A)
+≈ᴸ-refl = IsIndexedEquivalence.refl ∘ IndexedSetoid.isEquivalence
 
-_∈_ : ∀ {a aℓ} → List A → Language a aℓ → Set a
-l ∈ A = 𝕃 A l
+≈ᴸ-sym : ∀ {a aℓ} → (A : Language a aℓ) → Symmetric (𝕃 A) (≈ᴸ A)
+≈ᴸ-sym = IsIndexedEquivalence.sym ∘ IndexedSetoid.isEquivalence
 
-∅ : Language 0ℓ 0ℓ
-∅ = record
-  { 𝕃 = const ⊥
-  ; _≈ᴸ_ = ≡._≡_
-  ; ⤖ = const id
-  ; isLanguage = record
-    { ≈ᴸ-isEquivalence = ≡.isEquivalence
-    ; ⤖-cong = ≡.cong id
-    ; ⤖-bijective = (λ {x} → ⊥-elim x) , (λ ())
-    ; ⤖-refl = λ {_} {l∈𝕃} → ⊥-elim l∈𝕃
-    ; ⤖-sym = λ {_} {_} {l₁∈𝕃} → ⊥-elim l₁∈𝕃
-    ; ⤖-trans = λ {_} {_} {_} {l₁∈𝕃} → ⊥-elim l₁∈𝕃
-    }
+≈ᴸ-trans : ∀ {a aℓ} → (A : Language a aℓ) → Transitive (𝕃 A) (≈ᴸ A)
+≈ᴸ-trans = IsIndexedEquivalence.trans ∘ IndexedSetoid.isEquivalence
+
+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
+    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
+  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)
+
+≈-refl : ∀ {a aℓ} → B.Reflexive (_≈_ {a} {aℓ})
+≈-refl {x = A} = record
+  { f = id
+  ; f⁻¹ = id
+  ; cong₁ = id
+  ; cong₂ = id
   }
 
-⦃ε⦄ : Language (c ⊔ ℓ) (c ⊔ ℓ)
-⦃ε⦄ = record
-  { 𝕃 = [] ≋_
-  ; _≈ᴸ_ = ≡._≡_
-  ; ⤖ = flip ≋-trans
-  ; isLanguage = record
-    { ≈ᴸ-isEquivalence = ≡.isEquivalence
-    ; ⤖-cong = λ {_} {_} {l₁≋l₂} → ≡.cong (flip ≋-trans l₁≋l₂)
-    ; ⤖-bijective = λ {_} {_} {l₁≋l₂} →
-                  ( (λ {x} {y} x≡y → case x , y return (λ (x , y) → x ≡.≡ y) of λ { ([] , []) → ≡.refl })
-                  , (λ { [] → (case l₁≋l₂ return (λ x → ∃[ y ](≋-trans y x ≡.≡ [])) of λ { [] → [] , ≡.refl})}))
-    ; ⤖-refl = λ {_} {[]≋l} → case []≋l return (λ []≋l → ≋-trans []≋l ≋-refl ≡.≡ []≋l) of λ {[] → ≡.refl}
-    ; ⤖-sym = λ {_} {_} {[]≋l₁} {[]≋l₂} {l₁≋l₂} _ →
-      case []≋l₁ , []≋l₂ , l₁≋l₂
-      return (λ ([]≋l₁ , []≋l₂ , l₁≋l₂) → ≋-trans []≋l₂ (≋-sym l₁≋l₂) ≡.≡ []≋l₁)
-      of λ { ([] , [] , []) → ≡.refl }
-    ; ⤖-trans = λ {_} {_} {_} {[]≋l₁} {[]≋l₂} {[]≋l₃} {l₁≋l₂} {l₂≋l₃} _ _ →
-      case []≋l₁ , []≋l₂ , []≋l₃ , l₁≋l₂ , l₂≋l₃
-      return (λ ([]≋l₁ , []≋l₂ , []≋l₃ , l₁≋l₂ , l₂≋l₃) → ≋-trans []≋l₁ (≋-trans l₁≋l₂ l₂≋l₃) ≡.≡ []≋l₃)
-      of λ { ([] , [] , [] , [] , []) → ≡.refl }
+≈-sym : ∀ {a aℓ b bℓ} → B.Sym (_≈_ {a} {aℓ} {b} {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ℓ} → B.Trans (_≈_ {a} {aℓ}) (_≈_ {b} {bℓ} {c} {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
+
+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
     }
   }
 
-_≤_ : {a aℓ b bℓ : Level} → REL (Language a aℓ) (Language b bℓ) (c ⊔ a ⊔ b)
-A ≤ B = ∀ {l} → l ∈ A → l ∈ B
+≤-refl : ∀ {a aℓ} → B.Reflexive (_≤_ {a} {aℓ})
+≤-refl = record
+  { f = id
+  ; cong = id
+  }
+
+≤-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
+  ; cong = B≤C.cong ∘ A≤B.cong
+  }
+  where
+  module A≤B = _≤_ A≤B
+  module B≤C = _≤_ B≤C
+
+≤-antisym : ∀ {a aℓ b bℓ} → B.Antisym (_≤_ {a} {aℓ} {b} {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ℓ} → B.Min (_≤_ {b = b} {bℓ}) ∅
+≤-min A = record
+  { f = λ ()
+  ; cong = λ {_} {_} {}
+  }
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index b75f822..29e635d 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -4,56 +4,37 @@ open import Relation.Binary
 import Cfe.Language
 
 module Cfe.Language.Construct.Concatenate
-  {c ℓ a aℓ b bℓ} (setoid : Setoid c ℓ)
-  (A : Cfe.Language.Language setoid a aℓ)
-  (B : Cfe.Language.Language setoid b bℓ)
+  {c ℓ a aℓ b bℓ} (over : Setoid c ℓ)
+  (A : Cfe.Language.Language over a aℓ)
+  (B : Cfe.Language.Language over b bℓ)
   where
 
 open import Data.Empty
 open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid setoid
+open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Product as Product
 open import Function
 open import Level
-open import Cfe.Language setoid
-open Language
+open import Cfe.Language over
 
-open Setoid setoid renaming (Carrier to C)
+open Setoid over renaming (Carrier to C)
 
 infix 4 _≈ᶜ_
 infix 4 _∙_
 
 Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
-Concat l = ∃[ l₁ ](l₁ ∈ A × ∃[ l₂ ](l₂ ∈ B × (l₁ ++ l₂ ≋ l)))
+Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B ×  l₁ ++ l₂ ≋ l
 
-_≈ᶜ_ : {l : List C} → Rel (Concat l) (c ⊔ ℓ ⊔ aℓ ⊔ bℓ)
-(l₁ , l₁∈A , l₂ , l₂∈B , l₁++l₂) ≈ᶜ (l₁′ , l₁′∈A , l₂′ , l₂′∈B , l₁′++l₂′) =
-    ∃[ l₁≋l₁′ ](_≈ᴸ_ A (⤖ A l₁≋l₁′ l₁∈A) l₁′∈A)
-  × ∃[ l₂≋l₂′ ](_≈ᴸ_ B (⤖ B l₂≋l₂′ 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)
 
-⤖ᶜ : {l₁ l₂ : List C} → l₁ ≋ l₂ → Concat l₁ → Concat l₂
-⤖ᶜ l₁≋l₂ = map₂ (map₂ (map₂ (map₂ (flip ≋-trans l₁≋l₂))))
-
-_∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b) (c ⊔ ℓ ⊔ aℓ ⊔ bℓ)
+_∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b) (aℓ ⊔ bℓ)
 _∙_ = record
-  { 𝕃 = Concat
-  ; _≈ᴸ_ = _≈ᶜ_
-  ; ⤖ = ⤖ᶜ
-  ; isLanguage = record
-    { ≈ᴸ-isEquivalence = record
-      { refl = (≋-refl , ⤖-refl A) , (≋-refl , ⤖-refl B)
-      ; sym = Product.map (Product.map ≋-sym (⤖-sym A))
-                          (Product.map ≋-sym (⤖-sym B))
-      ; trans = Product.zip (Product.zip ≋-trans (⤖-trans A))
-                            (Product.zip ≋-trans (⤖-trans B))
-      }
-    ; ⤖-cong = id
-    ; ⤖-bijective = λ {_} {_} {l₁≋l₂} → id , λ l₂∈𝕃 →
-        ⤖ᶜ (≋-sym l₁≋l₂) l₂∈𝕃 , (≋-refl , ⤖-refl A) , (≋-refl , ⤖-refl B)
-    ; ⤖-refl = (≋-refl , ⤖-refl A) , (≋-refl , ⤖-refl B)
-    ; ⤖-sym = Product.map (Product.map ≋-sym (⤖-sym A))
-                          (Product.map ≋-sym (⤖-sym B))
-    ; ⤖-trans = Product.zip (Product.zip ≋-trans (⤖-trans A))
-                            (Product.zip ≋-trans (⤖-trans B))
+  { Carrier = Concat
+  ; _≈_ = _≈ᶜ_
+  ; isEquivalence = record
+    { refl = ≈ᴸ-refl A , ≈ᴸ-refl B
+    ; sym = Product.map (≈ᴸ-sym A) (≈ᴸ-sym B)
+    ; trans = Product.zip (≈ᴸ-trans A) (≈ᴸ-trans B)
     }
   }
diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda
index f54e015..daa1628 100644
--- a/src/Cfe/Language/Construct/Single.agda
+++ b/src/Cfe/Language/Construct/Single.agda
@@ -5,56 +5,47 @@ open import Relation.Binary
 import Relation.Binary.PropositionalEquality as ≡
 
 module Cfe.Language.Construct.Single
-  {a ℓ} (setoid : Setoid a ℓ)
-  (≈-trans-bijₗ : ∀ {a b c : Setoid.Carrier setoid}
-                  → {b≈c : Setoid._≈_ setoid b c}
-                  → Bijective ≡._≡_ ≡._≡_ (flip (Setoid.trans setoid {a}) b≈c))
-  (≈-trans-reflₗ : ∀ {a b : Setoid.Carrier setoid} {a≈b : Setoid._≈_ setoid a b}
-                   → Setoid.trans setoid a≈b (Setoid.refl setoid) ≡.≡ a≈b)
-  (≈-trans-symₗ : ∀ {a b c : Setoid.Carrier setoid}
-                  → {a≈b : Setoid._≈_ setoid a b}
-                  → {a≈c : Setoid._≈_ setoid a c}
-                  → {b≈c : Setoid._≈_ setoid b c}
-                  → Setoid.trans setoid a≈b b≈c ≡.≡ a≈c
-                  → Setoid.trans setoid a≈c (Setoid.sym setoid b≈c) ≡.≡ a≈b)
-  (≈-trans-transₗ : ∀ {a b c d : Setoid.Carrier setoid}
-                  → {a≈b : Setoid._≈_ setoid a b}
-                  → {a≈c : Setoid._≈_ setoid a c}
-                  → {a≈d : Setoid._≈_ setoid a d}
-                  → {b≈c : Setoid._≈_ setoid b c}
-                  → {c≈d : Setoid._≈_ setoid c d}
-                  → Setoid.trans setoid a≈b b≈c ≡.≡ a≈c
-                  → Setoid.trans setoid a≈c c≈d ≡.≡ a≈d
-                  → Setoid.trans setoid a≈b (Setoid.trans setoid b≈c c≈d) ≡.≡ a≈d)
+  {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 setoid renaming (Carrier to A)
+open Setoid over renaming (Carrier to C)
 
-open import Cfe.Language setoid
+open import Cfe.Language over hiding (_≈_)
 open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid setoid
+open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Product as Product
 open import Level
 
 private
-  ∷-inj : {a b : A} {l₁ l₂ : List A} {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 : {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 A} → {l₁≋l₂ : l₁ ≋ l₂} → Injective ≡._≡_ ≡._≡_ (flip (≋-trans {x}) l₁≋l₂)
+  ≋-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 A} → {l₁≋l₂ : l₁ ≋ l₂} → Surjective {A = x ≋ l₁} ≡._≡_ ≡._≡_ (flip (≋-trans {x}) l₁≋l₂)
+  ≋-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 A} {l₁≋l₂ : l₁ ≋ l₂} → ≋-trans l₁≋l₂ ≋-refl ≡.≡ l₁≋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 A} {l₁≋l₂ : l₁ ≋ l₂} {l₁≋l₃ : l₁ ≋ l₃} {l₂≋l₃ : l₂ ≋ l₃}
+  ≋-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
@@ -62,7 +53,7 @@ private
                                                    ∘ Product.map ≈-trans-symₗ ≋-trans-symₗ
                                                    ∘ ∷-inj
 
-  ≋-trans-transₗ : {l₁ l₂ l₃ l₄ : List A}
+  ≋-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₄
@@ -72,17 +63,13 @@ private
                                                                  ∘₂ uncurry (Product.zip ≈-trans-transₗ ≋-trans-transₗ)
                                                                  ∘₂ curry (Product.map ∷-inj ∷-inj)
 
-｛_｝ : List A → Language (a ⊔ ℓ) (a ⊔ ℓ)
-｛ l ｝ = record
-  { 𝕃 = l ≋_
-  ; _≈ᴸ_ = ≡._≡_
-  ; ⤖ = flip ≋-trans
-  ; isLanguage = record
-    { ≈ᴸ-isEquivalence = ≡.isEquivalence
-    ; ⤖-cong = λ {_} {_} {l₁≋l₂} → ≡.cong (flip ≋-trans l₁≋l₂)
-    ; ⤖-bijective = ≋-trans-injₗ , ≋-trans-surₗ
-    ; ⤖-refl = ≋-trans-reflₗ
-    ; ⤖-sym = ≋-trans-symₗ
-    ; ⤖-trans = ≋-trans-transₗ
+｛_｝ : C → Language (c ⊔ ℓ) (c ⊔ ℓ)
+｛ c ｝ = record
+  { Carrier = [ c ] ≋_
+  ; _≈_ = λ l≋m l≋n → ∃[ m≋n ] ≋-trans l≋m m≋n ≡.≡ l≋n
+  ; isEquivalence = record
+    { refl = ≋-refl , ≋-trans-reflₗ
+    ; sym = Product.map ≋-sym ≋-trans-symₗ
+    ; trans = Product.zip ≋-trans ≋-trans-transₗ
     }
   }
diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda
index 44d4c3f..ee8b0f7 100644
--- a/src/Cfe/Language/Construct/Union.agda
+++ b/src/Cfe/Language/Construct/Union.agda
@@ -4,99 +4,56 @@ open import Relation.Binary
 import Cfe.Language
 
 module Cfe.Language.Construct.Union
-  {c ℓ a aℓ b bℓ} (setoid : Setoid c ℓ)
-  (A : Cfe.Language.Language setoid a aℓ)
-  (B : Cfe.Language.Language setoid b bℓ)
+  {c ℓ a aℓ b bℓ} (over : Setoid c ℓ)
+  (A : Cfe.Language.Language over a aℓ)
+  (B : Cfe.Language.Language over b bℓ)
   where
 
 open import Data.Empty
 open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid setoid
+open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Product as Product
 open import Data.Sum as Sum
 open import Function
 open import Level
-open import Cfe.Language setoid
-open Language
+open import Cfe.Language over hiding (Lift)
 
-open Setoid setoid renaming (Carrier to C)
+open Setoid over renaming (Carrier to C)
 
 infix 4 _≈ᵁ_
 infix 4 _∪_
 
 Union : List C → Set (a ⊔ b)
-Union l = 𝕃 A l ⊎ 𝕃 B l
+Union l = l ∈ A ⊎ l ∈ B
 
-_≈ᵁ_ : {l : List C} → Rel (Union l) (aℓ ⊔ bℓ)
-(inj₁ x) ≈ᵁ (inj₁ y) = Lift bℓ (_≈ᴸ_ A x y)
+_≈ᵁ_ : {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)
-
-⤖ᵁ : {l₁ l₂ : List C} → l₁ ≋ l₂ → Union l₁ → Union l₂
-⤖ᵁ l₁≋l₂ = Sum.map (⤖ A l₁≋l₂) (⤖ B l₁≋l₂)
+(inj₂ x) ≈ᵁ (inj₂ y) = Lift aℓ (≈ᴸ B x y)
 
 _∪_ : Language (a ⊔ b) (aℓ ⊔ bℓ)
 _∪_ = record
-  { 𝕃 = Union
-  ; _≈ᴸ_ = _≈ᵁ_
-  ; ⤖ = ⤖ᵁ
-  ; isLanguage = record
-    { ≈ᴸ-isEquivalence = record
-      { refl = λ {x} → case x return (λ x → _≈ᵁ_ x x) of λ
-        { (inj₁ x) → lift (≈ᴸ-refl A)
-        ; (inj₂ y) → lift (≈ᴸ-refl B)
-        }
-      ; 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)
-          }
-      ; trans = λ {i} {j} {k} i≈ᵁj j≈ᵁk →
-        case ∃[ i ](∃[ j ](∃[ k ](i ≈ᵁ j × j ≈ᵁ k))) ∋ i , j , k , i≈ᵁj , j≈ᵁk
-        return (λ (i , _ , k , _) → i ≈ᵁ k) 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)
-          }
-      }
-    ; ⤖-cong = λ {_} {_} {l₁≋l₂} {x} {y} x≈ᵁy →
-      case ∃[ x ](∃[ y ](x ≈ᵁ y)) ∋ x , y , x≈ᵁy
-      return (λ (x , y , _) → (_≈ᵁ_ on ⤖ᵁ l₁≋l₂) x y) of λ
-        { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (⤖-cong A x≈ᵁy)
-        ; (inj₂ x , inj₂ y , lift x≈ᵁy) → lift (⤖-cong B x≈ᵁy)
-        }
-    ; ⤖-bijective = λ {_} {_} {l₁≋l₂} →
-      ( λ {x} {y} x≈ᵁy →
-        case ∃[ x ](∃[ y ]((_≈ᵁ_ on ⤖ᵁ l₁≋l₂) x y)) ∋ x , y , x≈ᵁy
-        return (λ (x , y , _) → x ≈ᵁ y) of λ
-          { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (⤖-injective A x≈ᵁy)
-          ; (inj₂ x , inj₂ y , lift x≈ᵁy) → lift (⤖-injective B x≈ᵁy)
-          })
-    , ( λ
-        { (inj₁ x) → Product.map inj₁ lift (⤖-surjective A x)
-        ; (inj₂ x) → Product.map inj₂ lift (⤖-surjective B x)
-        })
-    ; ⤖-refl = λ {_} {x} → case x return (λ x → ⤖ᵁ ≋-refl x ≈ᵁ x) of λ
-      { (inj₁ x) → lift (⤖-refl A)
-      ; (inj₂ y) → lift (⤖-refl B)
+  { Carrier = Union
+  ; _≈_ = _≈ᵁ_
+  ; isEquivalence = record
+    { refl = λ {_} {x} → case x return (λ x → x ≈ᵁ x) of λ
+      { (inj₁ x) → lift (≈ᴸ-refl A)
+      ; (inj₂ y) → lift (≈ᴸ-refl B)
       }
-    ; ⤖-sym = λ {_} {_} {x} {y} {l₁≋l₂} x≈ᵁy →
-      case ∃[ x ](∃[ y ](⤖ᵁ l₁≋l₂ x ≈ᵁ y)) ∋ x , y , x≈ᵁy
-      return (λ (x , y , _) → ⤖ᵁ (≋-sym l₁≋l₂) y ≈ᵁ x) of λ
-        { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (⤖-sym A x≈ᵁy)
-        ; (inj₂ x , inj₂ y , lift x≈ᵁy) → lift (⤖-sym 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)
         }
-    ; ⤖-trans = λ {_} {_} {_} {x} {y} {z} {l₁≋l₂} {l₂≋l₃} x≈ᵁy y≈ᵁz →
-      case (∃[ x ](∃[ y ](∃[ z ]((⤖ᵁ l₁≋l₂ x ≈ᵁ y) × (⤖ᵁ l₂≋l₃ y ≈ᵁ z))))) ∋
-           x , y , z , x≈ᵁy , y≈ᵁz
-      return (λ (x , _ , z , _ , _) → ⤖ᵁ (≋-trans l₁≋l₂ l₂≋l₃) x ≈ᵁ z) of λ
-        { (inj₁ x , inj₁ y , inj₁ z , lift x≈ᵁy , lift y≈ᵁz) →
-          lift (⤖-trans A x≈ᵁy y≈ᵁz)
-        ; (inj₂ x , inj₂ y , inj₂ z , lift x≈ᵁy , lift y≈ᵁz) →
-          lift (⤖-trans B x≈ᵁy y≈ᵁz)
+    ; 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)
         }
     }
   }
diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
new file mode 100644
index 0000000..62a946e
--- /dev/null
+++ b/src/Cfe/Language/Indexed/Construct/Iterate.agda
@@ -0,0 +1,70 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary as B using (Setoid)
+
+module Cfe.Language.Indexed.Construct.Iterate
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+open Setoid over using () renaming (Carrier to C)
+
+open import Cfe.Language over
+open import Cfe.Language.Indexed.Homogeneous over
+open import Data.List
+open import Data.Nat as ℕ hiding (_⊔_)
+open import Data.Product as Product
+open import Function
+open import Level hiding (Lift) renaming (suc to lsuc)
+open import Relation.Binary.Indexed.Heterogeneous
+open import Relation.Binary.PropositionalEquality as ≡
+
+open IndexedLanguage
+
+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))
+  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)
+  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)
+  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
+    }
+  }
+  where
+  module Iter = IndexedLanguage (Iterate f)
diff --git a/src/Cfe/Language/Indexed/Homogeneous.agda b/src/Cfe/Language/Indexed/Homogeneous.agda
new file mode 100644
index 0000000..c032978
--- /dev/null
+++ b/src/Cfe/Language/Indexed/Homogeneous.agda
@@ -0,0 +1,47 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary as B using (Setoid)
+
+module Cfe.Language.Indexed.Homogeneous
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+open import Cfe.Language over
+open import Level
+open import Data.List
+open import Data.Product
+open import Relation.Binary.Indexed.Heterogeneous
+
+open _≈_
+
+open Setoid over using () renaming (Carrier to C)
+
+record IndexedLanguage i iℓ a aℓ : Set (ℓ ⊔ suc (c ⊔ i ⊔ iℓ ⊔ a ⊔ aℓ)) where
+  field
+    Carrierᵢ : Set i
+    _≈ᵢ_ : B.Rel Carrierᵢ iℓ
+    isEquivalenceᵢ : B.IsEquivalence _≈ᵢ_
+    F : Carrierᵢ → Language a 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
+
+  -- ≈ᵗ-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 = {!!}
+  --     }
+  --   }