1 files changed, 59 insertions, 0 deletions
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
new file mode 100644
index 0000000..b75f822
--- /dev/null
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -0,0 +1,59 @@
+{-# OPTIONS --without-K --safe #-}
+
+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ℓ)
+  where
+
+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 Cfe.Language setoid
+open Language
+
+open Setoid setoid 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)))
+
+_≈ᶜ_ : {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} → l₁ ≋ l₂ → Concat l₁ → Concat l₂
+⤖ᶜ l₁≋l₂ = map₂ (map₂ (map₂ (map₂ (flip ≋-trans l₁≋l₂))))
+
+_∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b) (c ⊔ ℓ ⊔ 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))
+    }
+  }