From 02a0f87be944b1d43fda265058b891f419d25b65 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 16 Mar 2021 18:45:27 +0000
Subject: Change Language definition to respects instead of custom congruence.

---
 src/Cfe/Language/Construct/Single.agda | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'src/Cfe/Language/Construct/Single.agda')

diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda
index b06be3d..ddea1a6 100644
--- a/src/Cfe/Language/Construct/Single.agda
+++ b/src/Cfe/Language/Construct/Single.agda
@@ -12,17 +12,16 @@ open Setoid over renaming (Carrier to C)
 
 open import Cfe.Language over hiding (_≈_)
 open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Product as Product
 open import Data.Unit
 open import Level
 
-｛_｝ : C → Language (c ⊔ ℓ) 0ℓ
+｛_｝ : C → Language (c ⊔ ℓ)
 ｛ c ｝ = record
-  { Carrier = λ l → ∃[ a ] (l ≡.≡ [ a ] × a ≈ c)
-  ; _≈_ = λ _ _ → ⊤
-  ; isEquivalence = record
-    { refl = tt
-    ; sym = λ _ → tt
-    ; trans = λ _ _ → tt
-    }
+  { 𝕃 = [ c ] ≋_
+  ; ∈-resp-≋ = λ l₁≋l₂ l₁∈｛c｝ → ≋-trans l₁∈｛c｝ l₁≋l₂
   }
+
+xy∉｛c｝ : ∀ c x y l → x ∷ y ∷ l ∉ ｛ c ｝
+xy∉｛c｝ c x y l (_ ∷ ())
-- 
cgit v1.2.3