Separate out some Language properties.

3 files changed, 109 insertions, 93 deletions

diff --git a/src/Cfe/Expression/Properties.agda b/src/Cfe/Expression/Properties.agda
index 8bdc635..9af0d70 100644
--- a/src/Cfe/Expression/Properties.agda
+++ b/src/Cfe/Expression/Properties.agda
@@ -10,7 +10,7 @@ open Setoid over using () renaming (Carrier to C)
 
 open import Algebra
 open import Cfe.Expression.Base over
-open import Cfe.Language.Base over as L
+open import Cfe.Language over as L
 import Cfe.Language.Construct.Concatenate over as ∙
 import Cfe.Language.Construct.Union over as ∪
 import Cfe.Language.Indexed.Construct.Iterate over as ⋃
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index e1f7cc7..c34de30 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -92,98 +92,6 @@ record _≈_ {a aℓ b bℓ} (A : Language a aℓ) (B : Language b bℓ) : Set (
     cong₁ : ∀ {l₁ l₂ l₁∈A l₂∈A} → ≈ᴸ A {l₁} {l₂} l₁∈A l₂∈A → ≈ᴸ B (f l₁∈A) (f l₂∈A)
     cong₂ : ∀ {l₁ l₂ l₁∈B l₂∈B} → ≈ᴸ B {l₁} {l₂} l₁∈B l₂∈B → ≈ᴸ A (f⁻¹ l₁∈B) (f⁻¹ l₂∈B)
 
-≈-refl : ∀ {a aℓ} → B.Reflexive (_≈_ {a} {aℓ})
-≈-refl {x = A} = record
-  { f = id
-  ; f⁻¹ = id
-  ; cong₁ = id
-  ; cong₂ = id
-  }
-
-≈-sym : ∀ {a aℓ b bℓ} → B.Sym (_≈_ {a} {aℓ} {b} {bℓ}) _≈_
-≈-sym A≈B = record
-  { f = A≈B.f⁻¹
-  ; f⁻¹ = A≈B.f
-  ; cong₁ = A≈B.cong₂
-  ; cong₂ = A≈B.cong₁
-  }
-  where
-  module A≈B = _≈_ A≈B
-
-≈-trans : ∀ {a aℓ b bℓ c cℓ} → B.Trans (_≈_ {a} {aℓ}) (_≈_ {b} {bℓ} {c} {cℓ}) _≈_
-≈-trans {i = A} {B} {C} A≈B B≈C = record
-  { f = B≈C.f ∘ A≈B.f
-  ; f⁻¹ = A≈B.f⁻¹ ∘ B≈C.f⁻¹
-  ; cong₁ = B≈C.cong₁ ∘ A≈B.cong₁
-  ; cong₂ = A≈B.cong₂ ∘ B≈C.cong₂
-  }
-  where
-  module A≈B = _≈_ A≈B
-  module B≈C = _≈_ B≈C
-
-≈-isEquivalence : ∀ {a aℓ} → B.IsEquivalence (_≈_ {a} {aℓ} {a} {aℓ})
-≈-isEquivalence = record
-  { refl = ≈-refl
-  ; sym = ≈-sym
-  ; trans = ≈-trans
-  }
-
-setoid : ∀ a aℓ → B.Setoid (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ)
-setoid a aℓ = record { isEquivalence = ≈-isEquivalence {a} {aℓ} }
-
-≤-refl : ∀ {a aℓ} → B.Reflexive (_≤_ {a} {aℓ})
-≤-refl = record
-  { f = id
-  ; cong = id
-  }
-
-≤-reflexive : ∀ {a aℓ b bℓ} → _≈_ {a} {aℓ} {b} {bℓ} B.⇒ _≤_
-≤-reflexive A≈B = record
-  { f = A≈B.f
-  ; cong = A≈B.cong₁
-  }
-  where
-  module A≈B = _≈_ A≈B
-
-≤-trans : ∀ {a aℓ b bℓ c cℓ} → B.Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_
-≤-trans A≤B B≤C = record
-  { f = B≤C.f ∘ A≤B.f
-  ; cong = B≤C.cong ∘ A≤B.cong
-  }
-  where
-  module A≤B = _≤_ A≤B
-  module B≤C = _≤_ B≤C
-
-≤-antisym : ∀ {a aℓ b bℓ} → B.Antisym (_≤_ {a} {aℓ} {b} {bℓ}) _≤_ _≈_
-≤-antisym A≤B B≤A = record
-  { f = A≤B.f
-  ; f⁻¹ = B≤A.f
-  ; cong₁ = A≤B.cong
-  ; cong₂ = B≤A.cong
-  }
-  where
-  module A≤B = _≤_ A≤B
-  module B≤A = _≤_ B≤A
-
-≤-min : ∀ {b bℓ} → B.Min (_≤_ {b = b} {bℓ}) ∅
-≤-min A = record
-  { f = λ ()
-  ; cong = λ {_} {_} {}
-  }
-
-≤-isPartialOrder : ∀ a aℓ → B.IsPartialOrder (_≈_ {a} {aℓ}) _≤_
-≤-isPartialOrder a aℓ = record
-  { isPreorder = record
-    { isEquivalence = ≈-isEquivalence
-    ; reflexive = ≤-reflexive
-    ; trans = ≤-trans
-    }
-  ; antisym = ≤-antisym
-  }
-
-poset : ∀ a aℓ → B.Poset (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ) (c ⊔ a ⊔ aℓ)
-poset a aℓ = record { isPartialOrder = ≤-isPartialOrder a aℓ }
-
 null : ∀ {a} {aℓ} → Language a aℓ → Set a
 null A = [] ∈ A
 
diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
new file mode 100644
index 0000000..325b410
--- /dev/null
+++ b/src/Cfe/Language/Properties.agda
@@ -0,0 +1,108 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Relation.Binary
+
+module Cfe.Language.Properties
+  {c ℓ} (over : Setoid c ℓ)
+  where
+
+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
+open import Level
+
+≈-refl : ∀ {a aℓ} → Reflexive (_≈_ {a} {aℓ})
+≈-refl {x = A} = record
+  { f = id
+  ; f⁻¹ = id
+  ; cong₁ = id
+  ; cong₂ = id
+  }
+
+≈-sym : ∀ {a aℓ b bℓ} → Sym (_≈_ {a} {aℓ} {b} {bℓ}) _≈_
+≈-sym A≈B = record
+  { f = A≈B.f⁻¹
+  ; f⁻¹ = A≈B.f
+  ; cong₁ = A≈B.cong₂
+  ; cong₂ = A≈B.cong₁
+  }
+  where
+  module A≈B = _≈_ A≈B
+
+≈-trans : ∀ {a aℓ b bℓ c cℓ} → Trans (_≈_ {a} {aℓ}) (_≈_ {b} {bℓ} {c} {cℓ}) _≈_
+≈-trans {i = A} {B} {C} A≈B B≈C = record
+  { f = B≈C.f ∘ A≈B.f
+  ; f⁻¹ = A≈B.f⁻¹ ∘ B≈C.f⁻¹
+  ; cong₁ = B≈C.cong₁ ∘ A≈B.cong₁
+  ; cong₂ = A≈B.cong₂ ∘ B≈C.cong₂
+  }
+  where
+  module A≈B = _≈_ A≈B
+  module B≈C = _≈_ B≈C
+
+≈-isEquivalence : ∀ {a aℓ} → IsEquivalence (_≈_ {a} {aℓ} {a} {aℓ})
+≈-isEquivalence = record
+  { refl = ≈-refl
+  ; sym = ≈-sym
+  ; trans = ≈-trans
+  }
+
+setoid : ∀ a aℓ → Setoid (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ)
+setoid a aℓ = record { isEquivalence = ≈-isEquivalence {a} {aℓ} }
+
+≤-refl : ∀ {a aℓ} → Reflexive (_≤_ {a} {aℓ})
+≤-refl = record
+  { f = id
+  ; cong = id
+  }
+
+≤-reflexive : ∀ {a aℓ b bℓ} → _≈_ {a} {aℓ} {b} {bℓ} ⇒ _≤_
+≤-reflexive A≈B = record
+  { f = A≈B.f
+  ; cong = A≈B.cong₁
+  }
+  where
+  module A≈B = _≈_ A≈B
+
+≤-trans : ∀ {a aℓ b bℓ c cℓ} → Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_
+≤-trans A≤B B≤C = record
+  { f = B≤C.f ∘ A≤B.f
+  ; cong = B≤C.cong ∘ A≤B.cong
+  }
+  where
+  module A≤B = _≤_ A≤B
+  module B≤C = _≤_ B≤C
+
+≤-antisym : ∀ {a aℓ b bℓ} → Antisym (_≤_ {a} {aℓ} {b} {bℓ}) _≤_ _≈_
+≤-antisym A≤B B≤A = record
+  { f = A≤B.f
+  ; f⁻¹ = B≤A.f
+  ; cong₁ = A≤B.cong
+  ; cong₂ = B≤A.cong
+  }
+  where
+  module A≤B = _≤_ A≤B
+  module B≤A = _≤_ B≤A
+
+≤-min : ∀ {b bℓ} → Min (_≤_ {b = b} {bℓ}) ∅
+≤-min A = record
+  { f = λ ()
+  ; cong = λ {_} {_} {}
+  }
+
+≤-isPartialOrder : ∀ a aℓ → IsPartialOrder (_≈_ {a} {aℓ}) _≤_
+≤-isPartialOrder a aℓ = record
+  { isPreorder = record
+    { isEquivalence = ≈-isEquivalence
+    ; reflexive = ≤-reflexive
+    ; trans = ≤-trans
+    }
+  ; antisym = ≤-antisym
+  }
+
+poset : ∀ a aℓ → Poset (suc (c ⊔ a ⊔ aℓ)) (c ⊔ ℓ ⊔ a ⊔ aℓ) (c ⊔ a ⊔ aℓ)
+poset a aℓ = record { isPartialOrder = ≤-isPartialOrder a aℓ }