Add types and satisfiability

3 files changed, 40 insertions, 0 deletions

diff --git a/src/Cfe/Language.agda b/src/Cfe/Language.agda
index 1cb52dc..7469ef5 100644
--- a/src/Cfe/Language.agda
+++ b/src/Cfe/Language.agda
@@ -7,3 +7,4 @@ module Cfe.Language
   where
 
 open import Cfe.Language.Base setoid public
+open import Cfe.Language.Properties setoid public
diff --git a/src/Cfe/Type.agda b/src/Cfe/Type.agda
new file mode 100644
index 0000000..06a64c5
--- /dev/null
+++ b/src/Cfe/Type.agda
@@ -0,0 +1,9 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Setoid)
+
+module Cfe.Type
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+open import Cfe.Type.Base public
diff --git a/src/Cfe/Type/Base.agda b/src/Cfe/Type/Base.agda
new file mode 100644
index 0000000..ea4a657
--- /dev/null
+++ b/src/Cfe/Type/Base.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary using (Setoid)
+
+module Cfe.Type.Base
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+open Setoid over using () renaming (Carrier to C)
+
+open import Cfe.Language over
+open import Data.Bool
+open import Level renaming (suc to lsuc)
+open import Relation.Unary
+
+infix 4 _⊨_
+
+record Type fℓ lℓ : Set (c ⊔ lsuc (fℓ ⊔ lℓ)) where
+  field
+    Null : Bool
+    First : Pred C fℓ
+    Flast : Pred C lℓ
+
+open Type public
+
+record _⊨_ {a} {aℓ} {fℓ} {lℓ} (A : Language a aℓ) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
+  field
+    n⇒n : null A → T (Null τ)
+    f⇒f : first A ⊆ First τ
+    l⇒l : flast A ⊆ Flast τ