Make languages records with more properties.

1 files changed, 24 insertions, 4 deletions

diff --git a/src/Cfe/Language/Properties.agda b/src/Cfe/Language/Properties.agda
index 8d024a8..52d4644 100644
--- a/src/Cfe/Language/Properties.agda
+++ b/src/Cfe/Language/Properties.agda
@@ -3,19 +3,39 @@
 open import Relation.Binary
 
 module Cfe.Language.Properties
-  {a ℓ} (setoid : Setoid a ℓ)
+  {c ℓ} {setoid : Setoid c ℓ}
   where
 
 open Setoid setoid renaming (Carrier to A)
-
 open import Cfe.Language setoid
+open Language
+
+open import Data.List
+open import Data.List.Relation.Binary.Equality.Setoid setoid
 open import Function
+open import Level
+open import Relation.Binary.Construct.InducedPoset
+
+_≤′_ : ∀ {a aℓ} → Rel (Language a aℓ) (c ⊔ a)
+_≤′_ = _≤_
 
 ------------------------------------------------------------------------
 -- Properties of _≤_
 
-≤-refl : Reflexive _≤_
+≤-refl : ∀ {a aℓ} → Reflexive (_≤′_ {a} {aℓ})
 ≤-refl = id
 
-≤-trans : Transitive _≤_
+≤-trans : ∀ {a b c aℓ bℓ cℓ} → Trans (_≤_ {a} {aℓ}) (_≤_ {b} {bℓ} {c} {cℓ}) _≤_
 ≤-trans A≤B B≤C = B≤C ∘ A≤B
+
+≤-poset : ∀ {a aℓ} → Poset (c ⊔ ℓ ⊔ suc (a ⊔ aℓ)) (c ⊔ a) (c ⊔ a)
+≤-poset {a} {aℓ} = InducedPoset (_≤′_ {a} {aℓ}) id (λ i≤j j≤k → j≤k ∘ i≤j)
+
+-- ------------------------------------------------------------------------
+-- -- Properties of _∪_
+
+-- ∪-cong-≤ : Congruent₂ _≤_ _∪_
+-- ∪-cong-≤ A≤B C≤D = map A≤B C≤D
+
+-- ∪-cong : Congruent₂ _≈_ _∪_
+-- ∪-cong {A} {B} {C} {D} = ≤-cong₂→≈-cong₂ {_∪_} (λ A≤B C≤D → map A≤B C≤D) {A} {B} {C} {D}