2 files changed, 117 insertions, 0 deletions
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 = {!!}
+  --     }
+  --   }