1 files changed, 96 insertions, 27 deletions
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index 2e77b11..c1ff398 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -3,47 +3,116 @@
 open import Relation.Binary
 
 module Cfe.Language.Base
-  {a ℓ} (setoid : Setoid a ℓ)
+  {c ℓ} (setoid : Setoid c ℓ)
   where
 
 open Setoid setoid renaming (Carrier to A)
 
-open import Data.Empty.Polymorphic
+open import Data.Empty
 open import Data.List
 open import Data.List.Relation.Binary.Equality.Setoid setoid
-open import Data.Nat hiding (_≤_; _⊔_)
-open import Data.Product
-open import Data.Sum
+open import Data.Product as Product
 open import Function
-open import Level renaming (suc to lsuc)
+open import Level
+import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.Indexed.Heterogeneous as I
 
-Language : Set (lsuc a ⊔ lsuc ℓ)
-Language = List A → Set (a ⊔ ℓ)
+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₃∈𝕃
 
-∅ : Language
-∅ = const ⊥
+  ≈ᴸ-refl : ∀ {l} → Reflexive (_≈ᴸ_ {l})
+  ≈ᴸ-refl = IsEquivalence.refl ≈ᴸ-isEquivalence
 
-｛ε｝ : Language
-｛ε｝ = [] ≋_
+  ≈ᴸ-sym : ∀ {l} → Symmetric (_≈ᴸ_ {l})
+  ≈ᴸ-sym = IsEquivalence.sym ≈ᴸ-isEquivalence
 
-｛_｝ : A → Language
-｛ a ｝ = [ a ] ≋_
+  ≈ᴸ-trans : ∀ {l} → Transitive (_≈ᴸ_ {l})
+  ≈ᴸ-trans = IsEquivalence.trans ≈ᴸ-isEquivalence
 
-infix 4 _∪_
-infix 4 _∙_
+  ≈ᴸ-reflexive : ∀ {l} → ≡._≡_ ⇒ (_≈ᴸ_ {l})
+  ≈ᴸ-reflexive = IsEquivalence.reflexive ≈ᴸ-isEquivalence
 
-_∪_ : Language → Language → Language
-(A ∪ B) l = A l ⊎ B l
+  ⤖-injective : ∀ {l₁ l₂ l₁≋l₂} → Injective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ l₁≋l₂)
+  ⤖-injective = proj₁ ⤖-bijective
 
-_∙_ : Language → Language → Language
-(A ∙ B) l = ∃[ l₁ ] ∃[ l₂ ] (A l₁ × B l₂ × l₁ ++ l₂ ≋ l)
+  ⤖-surjective : ∀ {l₁ l₂ l₁≋l₂} → Surjective (_≈ᴸ_ {l₁}) (_≈ᴸ_ {l₂}) (⤖ {l₁} l₁≋l₂)
+  ⤖-surjective = proj₂ ⤖-bijective
 
-iterate : (Language → Language) → ℕ → Language → Language
-iterate f ℕ.zero = id
-iterate f (suc n) = f ∘ iterate f n
+  ⤖-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
+    }
 
-fix : (Language → Language) → Language
-fix f l = ∃[ n ] iterate f n ∅ l
+  ⤖-reflexive : ∀ {l l∈𝕃 l∈𝕃′} → l∈𝕃 ≡.≡ l∈𝕃′ → ∃[ l≋l ]((⤖ {l} l≋l l∈𝕃) ≈ᴸ l∈𝕃′)
+  ⤖-reflexive = I.IsIndexedEquivalence.reflexive ⤖-isIndexedEquivalence
 
-_≤_ : Language → Language → Set (a ⊔ ℓ)
-A ≤ B = ∀ {l} → A l → B l
+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 𝕃 _≈ᴸ_ ⤖
+
+  open IsLanguage isLanguage public
+
+open Language
+
+infix 4 _∈_
+
+_∈_ : ∀ {a aℓ} → List A → Language a aℓ → Set a
+l ∈ A = 𝕃 A l
+
+∅ : 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₁∈𝕃
+    }
+  }
+
+⦃ε⦄ : 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 }
+    }
+  }
+
+_≤_ : {a aℓ b bℓ : Level} → REL (Language a aℓ) (Language b bℓ) (c ⊔ a ⊔ b)
+A ≤ B = ∀ {l} → l ∈ A → l ∈ B