Add type relations.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/Cfe/Type/Base.agda b/src/Cfe/Type/Base.agda
index 90506b7..371bc2f 100644
--- a/src/Cfe/Type/Base.agda
+++ b/src/Cfe/Type/Base.agda
@@ -53,3 +53,19 @@ record _⊨_ {a} {aℓ} {fℓ} {lℓ} (A : Language a aℓ) (τ : Type fℓ lℓ
     n⇒n : null A → T (Null τ)
     f⇒f : first A ⊆ First τ
     l⇒l : flast A ⊆ Flast τ
+
+record _⊛_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ lℓ₁ ⊔ fℓ₂) where
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
+
+  field
+    ∄[l₁∩f₂] : Empty (τ₁.Flast ∩ τ₂.First)
+    ¬n₁ : T (not τ₁.Null)
+
+record _#_ {fℓ₁} {lℓ₁} {fℓ₂} {lℓ₂} (τ₁ : Type fℓ₁ lℓ₁) (τ₂ : Type fℓ₂ lℓ₂) : Set (c ⊔ fℓ₁ ⊔ fℓ₂) where
+  module τ₁ = Type τ₁
+  module τ₂ = Type τ₂
+
+  field
+    ∄[f₁∩f₂] : Empty (τ₁.First ∩ τ₂.First)
+    ¬n₁∨¬n₂ : T (not (τ₁.Null 𝔹.∨ τ₂.Null))