Introduce < for Languages.

Move around some definitions.

2 files changed, 30 insertions, 2 deletions

diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index a3b5136..71ee7df 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -63,6 +63,13 @@ record _≈_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔
     f : ∀ {l} → l ∈ A → l ∈ B
     f⁻¹ : ∀ {l} → l ∈ B → l ∈ A
 
+record _<_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔ b) where
+  field
+    f : ∀ {l} → l ∈ A → l ∈ B
+    l : List C
+    l∉A : l ∉ A
+    l∈B : l ∈ B
+
 null : ∀ {a} → Language a → Set a
 null A = [] ∈ A
 
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index 756877c..52b5470 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -8,8 +8,6 @@ module Cfe.Language.Properties
 
 open Setoid over using () renaming (Carrier to C)
 open import Cfe.Language.Base over
--- open Language
-
 open import Data.List
 open import Data.List.Relation.Binary.Equality.Setoid over
 open import Function
@@ -95,6 +93,29 @@ setoid a = record { isEquivalence = ≈-isEquivalence {a} }
 poset : ∀ a → Poset (c ⊔ ℓ ⊔ suc a) (c ⊔ ℓ ⊔ a) (c ⊔ a)
 poset a = record { isPartialOrder = ≤-isPartialOrder a }
 
+<-trans : ∀ {a b c} → Trans (_<_ {a}) (_<_ {b} {c}) _<_
+<-trans A<B B<C = record
+  { f = B<C.f ∘ A<B.f
+  ; l = A<B.l
+  ; l∉A = A<B.l∉A
+  ; l∈B = B<C.f A<B.l∈B
+  }
+  where
+  module A<B = _<_ A<B
+  module B<C = _<_ B<C
+
+<-irrefl : ∀ {a b} → Irreflexive (_≈_ {a} {b}) _<_
+<-irrefl A≈B A<B = A<B.l∉A (A≈B.f⁻¹ A<B.l∈B)
+  where
+  module A≈B = _≈_ A≈B
+  module A<B = _<_ A<B
+
+<-asym : ∀ {a} → Asymmetric (_<_ {a})
+<-asym A<B B<A = A<B.l∉A (B<A.f A<B.l∈B)
+  where
+  module A<B = _<_ A<B
+  module B<A = _<_ B<A
+
 lift-cong : ∀ {a} b (L : Language a) → Lift b L ≈ L
 lift-cong b L = record
   { f = lower