1 files changed, 108 insertions, 0 deletions
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ℓ }