diff options
Diffstat (limited to 'src/Cfe/Language/Construct/Union.agda')
| -rw-r--r-- | src/Cfe/Language/Construct/Union.agda | 110 |
1 files changed, 73 insertions, 37 deletions
diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda index ee8b0f7..4ed0774 100644 --- a/src/Cfe/Language/Construct/Union.agda +++ b/src/Cfe/Language/Construct/Union.agda @@ -1,14 +1,12 @@ {-# OPTIONS --without-K --safe #-} open import Relation.Binary -import Cfe.Language module Cfe.Language.Construct.Union - {c ℓ a aℓ b bℓ} (over : Setoid c ℓ) - (A : Cfe.Language.Language over a aℓ) - (B : Cfe.Language.Language over b bℓ) + {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 @@ -16,44 +14,82 @@ open import Data.Product as Product open import Data.Sum as Sum open import Function open import Level -open import Cfe.Language over hiding (Lift) +open import Cfe.Language over as 𝕃 hiding (Lift) open Setoid over renaming (Carrier to C) -infix 4 _≈ᵁ_ -infix 4 _∪_ - -Union : List C → Set (a ⊔ b) -Union l = l ∈ A ⊎ l ∈ B - -_≈ᵁ_ : {l₁ l₂ : List C} → REL (Union l₁) (Union l₂) (aℓ ⊔ bℓ) -(inj₁ x) ≈ᵁ (inj₁ y) = Lift bℓ (≈ᴸ A x y) -(inj₁ _) ≈ᵁ (inj₂ _) = Lift (aℓ ⊔ bℓ) ⊥ -(inj₂ _) ≈ᵁ (inj₁ _) = Lift (aℓ ⊔ bℓ) ⊥ -(inj₂ x) ≈ᵁ (inj₂ y) = Lift aℓ (≈ᴸ B x y) - -_∪_ : Language (a ⊔ b) (aℓ ⊔ bℓ) -_∪_ = record - { Carrier = Union - ; _≈_ = _≈ᵁ_ - ; isEquivalence = record - { refl = λ {_} {x} → case x return (λ x → x ≈ᵁ x) of λ - { (inj₁ x) → lift (≈ᴸ-refl A) - ; (inj₂ y) → lift (≈ᴸ-refl B) +module _ + {a aℓ b bℓ} + (A : Language a aℓ) + (B : Language b bℓ) + where + + infix 4 _≈ᵁ_ + infix 4 _∪_ + + Union : List C → Set (a ⊔ b) + Union l = l ∈ A ⊎ l ∈ B + + data _≈ᵁ_ : {l₁ l₂ : List C} → REL (Union l₁) (Union l₂) (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) where + A≈A : ∀ {l₁ l₂ x y} → ≈ᴸ A {l₁} {l₂} x y → (inj₁ x) ≈ᵁ (inj₁ y) + B≈B : ∀ {l₁ l₂ x y} → ≈ᴸ B {l₁} {l₂} x y → (inj₂ x) ≈ᵁ (inj₂ y) + + _∪_ : Language (a ⊔ b) (c ⊔ a ⊔ aℓ ⊔ b ⊔ bℓ) + _∪_ = record + { Carrier = Union + ; _≈_ = _≈ᵁ_ + ; isEquivalence = record + { refl = λ {_} {x} → case x return (λ x → x ≈ᵁ x) of λ { (inj₁ x) → A≈A (≈ᴸ-refl A) ; (inj₂ y) → B≈B (≈ᴸ-refl B)} + ; sym = λ { (A≈A x) → A≈A (≈ᴸ-sym A x) ; (B≈B x) → B≈B (≈ᴸ-sym B x)} + ; trans = λ { (A≈A x) (A≈A y) → A≈A (≈ᴸ-trans A x y) ; (B≈B x) (B≈B y) → B≈B (≈ᴸ-trans B x y) } } - ; sym = λ {_} {_} {x} {y} x≈ᵁy → - case (∃[ x ] ∃[ y ] x ≈ᵁ y ∋ x , y , x≈ᵁy) - return (λ (x , y , _) → y ≈ᵁ x) of λ - { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (≈ᴸ-sym A x≈ᵁy) - ; (inj₂ y₁ , inj₂ y , lift x≈ᵁy) → lift (≈ᴸ-sym B x≈ᵁy) + } + +isCommutativeMonoid : ∀ {a aℓ} → IsCommutativeMonoid 𝕃._≈_ _∪_ (𝕃.Lift a (c ⊔ a ⊔ 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) + ; cong₁ = λ { (A≈A x) → A≈A (_≈_.cong₁ X≈Y x) ; (B≈B x) → B≈B (_≈_.cong₁ U≈V x) } + ; cong₂ = λ { (A≈A x) → A≈A (_≈_.cong₂ X≈Y x) ; (B≈B x) → B≈B (_≈_.cong₂ U≈V x) } + } } - ; trans = λ {_} {_} {_} {x} {y} {z} x≈ᵁy y≈ᵁz → - case ∃[ x ] ∃[ y ] ∃[ z ] x ≈ᵁ y × y ≈ᵁ z ∋ x , y , z , x≈ᵁy , y≈ᵁz - return (λ (x , _ , z , _) → x ≈ᵁ z) of λ - { (inj₁ _ , inj₁ _ , inj₁ _ , lift x≈ᵁy , lift y≈ᵁz) → - lift (≈ᴸ-trans A x≈ᵁy y≈ᵁz) - ; (inj₂ _ , inj₂ _ , inj₂ _ , lift x≈ᵁy , lift y≈ᵁz) → - lift (≈ᴸ-trans B x≈ᵁy y≈ᵁz) + ; assoc = λ A B C → record + { f = Sum.assocʳ + ; f⁻¹ = Sum.assocˡ + ; cong₁ = λ { (A≈A (A≈A x)) → A≈A x ; (A≈A (B≈B x)) → B≈B (A≈A x) ; (B≈B x) → B≈B (B≈B x) } + ; cong₂ = λ { (A≈A x) → A≈A (A≈A x) ; (B≈B (A≈A x)) → A≈A (B≈B x) ; (B≈B (B≈B x)) → B≈B x } } + } + ; identity = (λ A → record + { f = λ { (inj₂ x) → x } + ; f⁻¹ = inj₂ + ; cong₁ = λ { (B≈B x) → x } + ; cong₂ = B≈B + }) , (λ A → record + { f = λ { (inj₁ x) → x } + ; f⁻¹ = inj₁ + ; cong₁ = λ { (A≈A x) → x } + ; cong₂ = A≈A + }) + } + ; comm = λ A B → record + { f = Sum.swap + ; f⁻¹ = Sum.swap + ; cong₁ = λ { (A≈A x) → B≈B x ; (B≈B x) → A≈A x } + ; cong₂ = λ { (A≈A x) → B≈B x ; (B≈B x) → A≈A x } } } + +∪-monotone : ∀ {a aℓ b bℓ} → _∪_ Preserves₂ _≤_ {a} {aℓ} ⟶ _≤_ {b} {bℓ} ⟶ _≤_ +∪-monotone X≤Y U≤V = record + { f = Sum.map X≤Y.f U≤V.f + ; cong = λ { (A≈A l₁≈l₂) → A≈A (X≤Y.cong l₁≈l₂) ; (B≈B l₁≈l₂) → B≈B (U≤V.cong l₁≈l₂)} + } + where + module X≤Y = _≤_ X≤Y + module U≤V = _≤_ U≤V |