Clean-up Language hierarchy.

1 files changed, 0 insertions, 88 deletions

diff --git a/src/Cfe/Language/Indexed/Construct/Iterate.agda b/src/Cfe/Language/Indexed/Construct/Iterate.agda
deleted file mode 100644
index 0ae9100..0000000
--- a/src/Cfe/Language/Indexed/Construct/Iterate.agda
+++ /dev/null
@@ -1,88 +0,0 @@
-{-# 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 Algebra
-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.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
-
-infix 9 _^_
-
-_^_ : ∀ {a} {A : Set a} → Op₁ A → ℕ → Op₁ A
-f ^ zero = id
-f ^ (suc n) = f ∘ (f ^ n)
-
-f-fn-x≡fn-f-x : ∀ {a} {A : Set a} (f : A → A) n x → f ((f ^ n) x) ≡ (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
-
-  private
-    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 → (f ^ n) x A.≈ (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
-
-  private
-    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 → (f ^ n) x A.≤ (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}
-  where
-  Iterate : (Language a → Language a) → IndexedLanguage 0ℓ 0ℓ a
-  Iterate f = record
-    { Carrierᵢ = ℕ
-    ; _≈ᵢ_ = ≡._≡_
-    ; isEquivalenceᵢ = ≡.isEquivalence
-    ; F = λ n → (f ^ n) (Lift a ∅)
-    ; cong = λ {≡.refl → ≈-refl}
-    }
-
-  ⋃ : (Language a → Language a) → Language a
-  ⋃ f = record
-    { 𝕃 = Iter.Tagged
-    ; ∈-resp-≋ = λ { l₁≋l₂ (i , l₁∈fi) → i , Language.∈-resp-≋ (Iter.F i) l₁≋l₂ l₁∈fi }
-    }
-    where
-    module Iter = IndexedLanguage (Iterate f)
-
-  fⁿ≤⋃f : ∀ f n → (f ^ n) (Lift a ∅) ≤ ⋃ f
-  fⁿ≤⋃f f n = record { f = n ,_ }
-
-  ⋃-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) 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}
-    }
-
-  ⋃-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 }
-    }