Change Language definition to respects instead of custom congruence.

2 files changed, 9 insertions, 15 deletions

diff --git a/src/Cfe/Type/Base.agda b/src/Cfe/Type/Base.agda
index 371bc2f..a5ed780 100644
--- a/src/Cfe/Type/Base.agda
+++ b/src/Cfe/Type/Base.agda
@@ -48,7 +48,7 @@ _∙_ {lℓ₁ = lℓ₁} {fℓ₂} {lℓ₂} τ₁ τ₂ = record
   ; Flast = Flast τ₂ ∪ (if Null τ₂ then First τ₂ ∪ Flast τ₁ else λ x → L.Lift (lℓ₁ ⊔ fℓ₂) (x U.∈ U.∅))
   }
 
-record _⊨_ {a} {aℓ} {fℓ} {lℓ} (A : Language a aℓ) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
+record _⊨_ {a} {fℓ} {lℓ} (A : Language a) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
   field
     n⇒n : null A → T (Null τ)
     f⇒f : first A ⊆ First τ
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 2222fbe..cfdf694 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -13,10 +13,11 @@ open import Cfe.Language.Construct.Single over
 open import Cfe.Type.Base over
 open import Data.Empty
 open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Product
 open import Function
 
-⊨-anticongˡ : ∀ {a aℓ b bℓ fℓ lℓ} {A : Language a aℓ} {B : Language b bℓ} {τ : Type fℓ lℓ} → B ≤ A → A ⊨ τ → B ⊨ τ
+⊨-anticongˡ : ∀ {a b fℓ lℓ} {A : Language a} {B : Language b} {τ : Type fℓ lℓ} → B ≤ A → A ⊨ τ → B ⊨ τ
 ⊨-anticongˡ B≤A A⊨τ = record
   { n⇒n = A⊨τ.n⇒n ∘ B≤A.f
   ; f⇒f = A⊨τ.f⇒f ∘ map₂ B≤A.f
@@ -26,12 +27,10 @@ open import Function
   module B≤A = _≤_ B≤A
   module A⊨τ = _⊨_ A⊨τ
 
-L⊨τ⊥⇒L≈∅ : ∀ {a aℓ} {L : Language a aℓ} → L ⊨ τ⊥ → L ≈ ∅
+L⊨τ⊥⇒L≈∅ : ∀ {a} {L : Language a} → L ⊨ τ⊥ → L ≈ ∅
 L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   { f = λ {l} → elim l
   ; f⁻¹ = λ ()
-  ; cong₁ = λ {l} {_} {l∈L} → ⊥-elim (elim l l∈L)
-  ; cong₂ = λ {_} {_} {}
   }
   where
   module L⊨τ⊥ = _⊨_ L⊨τ⊥
@@ -47,10 +46,9 @@ L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   ; l⇒l = λ ()
   }
 
-L⊨τε⇒L≤｛ε｝ : ∀ {a aℓ} {L : Language a aℓ} → L ⊨ τε → L ≤ ｛ε｝
+L⊨τε⇒L≤｛ε｝ : ∀ {a} {L : Language a} → L ⊨ τε → L ≤ ｛ε｝
 L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
   { f = λ {l} → elim l
-  ; cong = const tt
   }
   where
   open import Data.Unit
@@ -73,16 +71,12 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
 ｛c｝⊨τ[c] : ∀ c → ｛ c ｝ ⊨ τ[ c ]
 ｛c｝⊨τ[c] c = record
   { n⇒n = λ ()
-  ; f⇒f = λ {x} → λ {([] , (a , eq , a∼c)) → begin
-    c ≈˘⟨ a∼c ⟩
-    a ≡˘⟨ proj₁ (∷-injective eq) ⟩
-    x ∎}
-  ; l⇒l = λ
+  ; f⇒f = λ {x} → λ {([] , (c∼x ∷ []≋[])) → c∼x}
+  ; l⇒l = λ {x} → λ
     { ([] , []≢[] , _) → ⊥-elim ([]≢[] refl)
-    ; (x ∷ [] , x∷[]≢[] , ())
+    ; (y ∷ [] , _ , l′ , y∷x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y x l′ y∷x∷l′∈｛c｝)
+    ; (y ∷ z ∷ l , _ , l′ , y∷z∷l++x∷l′∈｛c｝) → ⊥-elim (xy∉｛c｝ c y z (l ++ x ∷ l′) y∷z∷l++x∷l′∈｛c｝)
     }
   }
   where
-  open import Data.List.Properties
-  open import Relation.Binary.Reasoning.Setoid over
   open import Relation.Binary.PropositionalEquality