From b7227fb6ecb7b54313b14bd50381bdb504f13d5c Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 5 Mar 2021 15:44:38 +0000
Subject: Prove satisfiability of τε.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

There is a small error in the paper. It claims that L⊨τε if and only if L≈{ε}.
However, from `⊨-anticongˡ` and `≤-min`, we have ∅⊨{ε}.
---
 src/Cfe/Type/Properties.agda | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'src/Cfe')

diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 14e871b..987e41f 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -45,3 +45,26 @@ L⊨τ⊥⇒L≈∅ {L = L} L⊨τ⊥ = record
   ; f⇒f = λ ()
   ; l⇒l = λ ()
   }
+
+L⊨τε⇒L≤｛ε｝ : ∀ {a aℓ} {L : Language a aℓ} → L ⊨ τε → L ≤ ｛ε｝
+L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
+  { f = λ {l} l∈L → elim l l∈L
+  ; cong = λ {l₁} {l₂} {l₁∈L} {l₂∈L} l₁≈l₂ → tt
+  }
+  where
+  open import Data.Unit
+  open import Relation.Binary.PropositionalEquality
+  module L⊨τε = _⊨_ L⊨τε
+
+  elim : ∀ l (l∈L : l ∈ L) → l ∈ ｛ε｝
+  elim [] []∈L = refl
+  elim (x ∷ l) xl∈L = ⊥-elim (L⊨τε.f⇒f (-, xl∈L))
+
+｛ε｝⊨τε : ｛ε｝ ⊨ τε
+｛ε｝⊨τε = record
+  { n⇒n = const tt
+  ; f⇒f = λ ()
+  ; l⇒l = λ { ([] , ()) ; (_ ∷ _ , ())}
+  }
+  where
+  open import Data.Unit
-- 
cgit v1.2.3