Change Language definition to respects instead of custom congruence.

1 files changed, 30 insertions, 65 deletions

diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index 74854df..bda9000 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --without-K --safe #-}
 
-open import Relation.Binary as B using (Setoid)
+open import Relation.Binary
 
 module Cfe.Language.Base
   {c ℓ} (over : Setoid c ℓ)
@@ -11,96 +11,61 @@ open Setoid over using () renaming (Carrier to C)
 open import Algebra
 open import Data.Empty
 open import Data.List hiding (null)
+open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Product
 open import Data.Unit using (⊤; tt)
-open import Function hiding (Injection; Surjection; Inverse)
-import Function.Equality as Equality using (setoid)
+open import Function hiding (_⟶_)
 open import Level as L hiding (Lift)
-open import Relation.Binary.Indexed.Heterogeneous.Construct.Trivial as Trivial
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
-open import Relation.Binary.Indexed.Heterogeneous
+open import Relation.Binary.PropositionalEquality
 
 infix 4 _∈_
 infix 4 _∉_
 
-Language : ∀ a aℓ → Set (suc c ⊔ suc a ⊔ suc aℓ)
-Language a aℓ = IndexedSetoid (List C) a aℓ
+record Language a : Set (c ⊔ ℓ ⊔ suc a) where
+  field
+    𝕃 : List C → Set a
+    ∈-resp-≋ : 𝕃 ⟶ 𝕃 Respects _≋_
 
-∅ : Language 0ℓ 0ℓ
-∅ = Trivial.indexedSetoid (≡.setoid ⊥)
+∅ : Language 0ℓ
+∅ = record
+  { 𝕃 = const ⊥
+  ; ∈-resp-≋ = λ _ ()
+  }
 
-｛ε｝ : Language c 0ℓ
+｛ε｝ : Language c
 ｛ε｝ = record
-  { Carrier = [] ≡_
-  ; _≈_ = λ _ _ → ⊤
-  ; isEquivalence = record
-    { refl = tt
-    ; sym = λ _ → tt
-    ; trans = λ _ _ → tt
-    }
+  { 𝕃 = [] ≡_
+  ; ∈-resp-≋ = λ { [] refl → refl}
   }
 
-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)
-    }
+Lift : ∀ {a} → (b : Level) → Language a → Language (a ⊔ b)
+Lift b A = record
+  { 𝕃 = L.Lift b ∘ A.𝕃
+  ; ∈-resp-≋ = λ { eq (lift l∈A) → lift (A.∈-resp-≋ eq l∈A)}
   }
   where
-  module A = IndexedSetoid A
-
-𝕃 : ∀ {a aℓ} → Language a aℓ → List C → Set a
-𝕃 = IndexedSetoid.Carrier
+  module A = Language A
 
-_∈_ : ∀ {a aℓ} → List C → Language a aℓ → Set a
-_∈_ = flip 𝕃
+_∈_ : ∀ {a} → List C → Language a → Set a
+_∈_ = flip Language.𝕃
 
-_∉_ : ∀ {a aℓ} → List C → Language a aℓ → Set a
+_∉_ : ∀ {a} → List C → Language a → Set a
 l ∉ A = l ∈ A → ⊥
 
-∈-cong : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → l₁ ≡ l₂ → l₁ ∈ A → l₂ ∈ A
-∈-cong A ≡.refl l∈A = l∈A
-
-≈ᴸ : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂} → 𝕃 A l₁ → 𝕃 A l₂ → Set aℓ
-≈ᴸ = IndexedSetoid._≈_
-
-≈ᴸ-refl : ∀ {a aℓ} → (A : Language a aℓ) → Reflexive (𝕃 A) (≈ᴸ A)
-≈ᴸ-refl = IsIndexedEquivalence.refl ∘ IndexedSetoid.isEquivalence
-
-≈ᴸ-sym : ∀ {a aℓ} → (A : Language a aℓ) → Symmetric (𝕃 A) (≈ᴸ A)
-≈ᴸ-sym = IsIndexedEquivalence.sym ∘ IndexedSetoid.isEquivalence
-
-≈ᴸ-trans : ∀ {a aℓ} → (A : Language a aℓ) → Transitive (𝕃 A) (≈ᴸ A)
-≈ᴸ-trans = IsIndexedEquivalence.trans ∘ IndexedSetoid.isEquivalence
-
-≈ᴸ-cong : ∀ {a aℓ} → (A : Language a aℓ) → ∀ {l₁ l₂ l₃ l₄} →
-          (l₁≡l₂ : l₁ ≡ l₂) → (l₃≡l₄ : l₃ ≡ l₄) →
-          (l₁∈A : l₁ ∈ A) → (l₃∈A : l₃ ∈ A) →
-          ≈ᴸ A l₁∈A l₃∈A →
-          ≈ᴸ A (∈-cong A l₁≡l₂ l₁∈A) (∈-cong A l₃≡l₄ l₃∈A)
-≈ᴸ-cong A ≡.refl ≡.refl l₁∈A l₃∈A eq = eq
-
-record _≤_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where
+record _≤_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ a ⊔ 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
+record _≈_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔ 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)
 
-null : ∀ {a} {aℓ} → Language a aℓ → Set a
+null : ∀ {a} → Language a → Set a
 null A = [] ∈ A
 
-first : ∀ {a} {aℓ} → Language a aℓ → C → Set (c ⊔ a)
+first : ∀ {a} → Language a → C → Set (c ⊔ a)
 first A x = ∃[ l ] x ∷ l ∈ A
 
-flast : ∀ {a} {aℓ} → Language a aℓ → C → Set (c ⊔ a)
-flast A x = ∃[ l ] (l ≡.≢ [] × ∃[ l′ ] l ++ x ∷ l′ ∈ A)
+flast : ∀ {a} → Language a → C → Set (c ⊔ a)
+flast A x = ∃[ l ] (l ≢ [] × ∃[ l′ ] l ++ x ∷ l′ ∈ A)