From da429008d25ac87ec67a4fb18a5cbee0ba756bcf Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 5 Apr 2021 14:31:57 +0100
Subject: Clean-up Language hierarchy.

---
 src/Cfe/Language/Construct/Union.agda | 84 -----------------------------------
 1 file changed, 84 deletions(-)
 delete mode 100644 src/Cfe/Language/Construct/Union.agda

(limited to 'src/Cfe/Language/Construct/Union.agda')

diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda
deleted file mode 100644
index 0865123..0000000
--- a/src/Cfe/Language/Construct/Union.agda
+++ /dev/null
@@ -1,84 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Relation.Binary
-
-module Cfe.Language.Construct.Union
-  {c ℓ} (over : Setoid c ℓ)
-  where
-
-open import Algebra
-open import Data.Empty
-open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid over
-open import Data.Product as Product
-open import Data.Sum as Sum
-open import Function
-open import Level
-open import Cfe.Language over as 𝕃 hiding (Lift)
-
-open Setoid over renaming (Carrier to C)
-
-module _
-  {a b}
-  (A : Language a)
-  (B : Language b)
-  where
-
-  private
-    module A = Language A
-    module B = Language B
-
-  infix 6 _∪_
-
-  Union : List C → Set (a ⊔ b)
-  Union l = l ∈ A ⊎ l ∈ B
-
-  _∪_ : Language (a ⊔ b)
-  _∪_ = record
-    { 𝕃 = Union
-    ; ∈-resp-≋ = λ l₁≋l₂ → Sum.map (A.∈-resp-≋ l₁≋l₂) (B.∈-resp-≋ l₁≋l₂)
-    }
-
-isCommutativeMonoid : ∀ {a} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a ∅)
-isCommutativeMonoid = record
-  { isMonoid = record
-    { isSemigroup = record
-      { isMagma = record
-        { isEquivalence = ≈-isEquivalence
-        ; ∙-cong = λ X≈Y U≈V → record
-          { f = Sum.map (_≈_.f X≈Y) (_≈_.f U≈V)
-          ; f⁻¹ = Sum.map (_≈_.f⁻¹ X≈Y) (_≈_.f⁻¹ U≈V)
-          }
-        }
-      ; assoc = λ A B C → record
-        { f = Sum.assocʳ
-        ; f⁻¹ = Sum.assocˡ
-        }
-      }
-    ; identity = (λ A → record
-      { f = λ { (inj₂ x) → x }
-      ; f⁻¹ = inj₂
-      }) , (λ A → record
-      { f = λ { (inj₁ x) → x }
-      ; f⁻¹ = inj₁
-      })
-    }
-  ; comm = λ A B → record
-    { f = Sum.swap
-    ; f⁻¹ = Sum.swap
-    }
-  }
-
-∪-mono : ∀ {a b} → _∪_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
-∪-mono X≤Y U≤V = record
-  { f = Sum.map X≤Y.f U≤V.f
-  }
-  where
-  module X≤Y = _≤_ X≤Y
-  module U≤V = _≤_ U≤V
-
-∪-unique : ∀ {a b} {A : Language a} {B : Language b} → (∀ x → first A x → first B x → ⊥) → (𝕃.null A → 𝕃.null B → ⊥) → ∀ {l} → l ∈ A ∪ B → (l ∈ A × l ∉ B) ⊎ (l ∉ A × l ∈ B)
-∪-unique fA∩fB≡∅ ¬nA∨¬nB {[]}    (inj₁ []∈A) = inj₁ ([]∈A , ¬nA∨¬nB []∈A)
-∪-unique fA∩fB≡∅ ¬nA∨¬nB {x ∷ l} (inj₁ xl∈A) = inj₁ (xl∈A , (λ xl∈B → fA∩fB≡∅ x (-, xl∈A) (-, xl∈B)))
-∪-unique fA∩fB≡∅ ¬nA∨¬nB {[]}    (inj₂ []∈B) = inj₂ (flip ¬nA∨¬nB []∈B , []∈B)
-∪-unique fA∩fB≡∅ ¬nA∨¬nB {x ∷ l} (inj₂ xl∈B) = inj₂ ((λ xl∈A → fA∩fB≡∅ x (-, xl∈A) (-, xl∈B)) , xl∈B)
-- 
cgit v1.2.3