From 9c5540562f53be81bfb03ef2b96d7f59b3ddea44 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Fri, 5 Mar 2021 00:10:08 +0000
Subject: Separate out some Language properties.

---
 src/Cfe/Language/Base.agda | 92 ----------------------------------------------
 1 file changed, 92 deletions(-)

(limited to 'src/Cfe/Language/Base.agda')

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
 
-- 
cgit v1.2.3