From 5302e4a27a64cb2a97120517df4b6998da7b3168 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Fri, 5 Mar 2021 00:00:04 +0000 Subject: Complete proofs up to Proposition 3.2 (excluding unrolling) --- src/Cfe/Language/Construct/Concatenate.agda | 130 +++++++++++++++++++++++----- src/Cfe/Language/Construct/Single.agda | 61 ++----------- src/Cfe/Language/Construct/Union.agda | 110 +++++++++++++++-------- 3 files changed, 189 insertions(+), 112 deletions(-) (limited to 'src/Cfe/Language/Construct') diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda index 29e635d..62acf8f 100644 --- a/src/Cfe/Language/Construct/Concatenate.agda +++ b/src/Cfe/Language/Construct/Concatenate.agda @@ -1,40 +1,128 @@ {-# OPTIONS --without-K --safe #-} open import Relation.Binary -import Cfe.Language module Cfe.Language.Construct.Concatenate - {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 Cfe.Language over as 𝕃 open import Data.Empty open import Data.List -open import Data.List.Relation.Binary.Equality.Setoid over +open import Data.List.Properties open import Data.Product as Product open import Function open import Level -open import Cfe.Language over +open import Relation.Binary.PropositionalEquality as ≡ +import Relation.Binary.Indexed.Heterogeneous as I -open Setoid over renaming (Carrier to C) +open Setoid over using () renaming (Carrier to C) -infix 4 _≈ᶜ_ -infix 4 _∙_ +module _ + {a aℓ b bℓ} + (A : Language a aℓ) + (B : Language b bℓ) + where + + infix 4 _≈ᶜ_ + infix 4 _∙_ + + Concat : List C → Set (c ⊔ a ⊔ b) + Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≡ l -Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b) -Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≋ l + _≈ᶜ_ : {l₁ l₂ : List C} → REL (Concat l₁) (Concat l₂) (aℓ ⊔ bℓ) + (_ , l₁∈A , _ , l₂∈B , _) ≈ᶜ (_ , l₁′∈A , _ , l₂′∈B , _) = (≈ᴸ A l₁∈A l₁′∈A) × (≈ᴸ B l₂∈B l₂′∈B) -_≈ᶜ_ : {l₁ l₂ : List C} → REL (Concat l₁) (Concat l₂) (aℓ ⊔ bℓ) -(_ , l₁∈A , _ , l₂∈B , _) ≈ᶜ (_ , l₁′∈A , _ , l₂′∈B , _) = (≈ᴸ A l₁∈A l₁′∈A) × (≈ᴸ B l₂∈B l₂′∈B) + _∙_ : Language (c ⊔ a ⊔ b) (aℓ ⊔ bℓ) + _∙_ = record + { Carrier = Concat + ; _≈_ = _≈ᶜ_ + ; isEquivalence = record + { refl = ≈ᴸ-refl A , ≈ᴸ-refl B + ; sym = Product.map (≈ᴸ-sym A) (≈ᴸ-sym B) + ; trans = Product.zip (≈ᴸ-trans A) (≈ᴸ-trans B) + } + } -_∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b) (aℓ ⊔ bℓ) -_∙_ = record - { Carrier = Concat - ; _≈_ = _≈ᶜ_ - ; isEquivalence = record - { refl = ≈ᴸ-refl A , ≈ᴸ-refl B - ; sym = Product.map (≈ᴸ-sym A) (≈ᴸ-sym B) - ; trans = Product.zip (≈ᴸ-trans A) (≈ᴸ-trans B) +isMonoid : ∀ {a aℓ} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) +isMonoid {a} = record + { isSemigroup = record + { isMagma = record + { isEquivalence = ≈-isEquivalence + ; ∙-cong = λ X≈Y U≈V → record + { f = λ { (l₁ , l₁∈X , l₂ , l₂∈U , l₁++l₂≡l) → l₁ , _≈_.f X≈Y l₁∈X , l₂ , _≈_.f U≈V l₂∈U , l₁++l₂≡l} + ; f⁻¹ = λ { (l₁ , l₁∈Y , l₂ , l₂∈V , l₁++l₂≡l) → l₁ , _≈_.f⁻¹ X≈Y l₁∈Y , l₂ , _≈_.f⁻¹ U≈V l₂∈V , l₁++l₂≡l} + ; cong₁ = λ { (x , y) → _≈_.cong₁ X≈Y x , _≈_.cong₁ U≈V y} + ; cong₂ = λ { (x , y) → _≈_.cong₂ X≈Y x , _≈_.cong₂ U≈V y} + } + } + ; assoc = λ X Y Z → record + { f = λ {l} → (λ { (l₁ , (l₁′ , l₁′∈X , l₂′ , l₂′∈Y , l₁′++l₂′≡l₁) , l₂ , l₂∈Z , l₁++l₂≡l) → + l₁′ , l₁′∈X , l₂′ ++ l₂ , (l₂′ , l₂′∈Y , l₂ , l₂∈Z , refl) , (begin + l₁′ ++ l₂′ ++ l₂ ≡˘⟨ ++-assoc l₁′ l₂′ l₂ ⟩ + (l₁′ ++ l₂′) ++ l₂ ≡⟨ cong (_++ l₂) l₁′++l₂′≡l₁ ⟩ + l₁ ++ l₂ ≡⟨ l₁++l₂≡l ⟩ + l ∎)}) + ; f⁻¹ = λ {l} → λ { (l₁ , l₁∈X , l₂ , (l₁′ , l₁′∈Y , l₂′ , l₂′∈Z , l₁′++l₂′≡l₂), l₁++l₂≡l) → + l₁ ++ l₁′ , ( l₁ , l₁∈X , l₁′ , l₁′∈Y , refl) , l₂′ , l₂′∈Z , (begin + (l₁ ++ l₁′) ++ l₂′ ≡⟨ ++-assoc l₁ l₁′ l₂′ ⟩ + l₁ ++ (l₁′ ++ l₂′) ≡⟨ cong (l₁ ++_) l₁′++l₂′≡l₂ ⟩ + l₁ ++ l₂ ≡⟨ l₁++l₂≡l ⟩ + l ∎)} + ; cong₁ = Product.assocʳ + ; cong₂ = Product.assocˡ + } } + ; identity = (λ A → record + { f = idˡ {a} A + ; f⁻¹ = λ {l} l∈A → [] , lift refl , l , l∈A , refl + ; cong₁ = λ {l₁} {l₂} {l₁∈A} {l₂∈A} → idˡ-cong {a} A {l₁} {l₂} {l₁∈A} {l₂∈A} + ; cong₂ = λ l₁≈l₂ → lift _ , l₁≈l₂ + }) , (λ A → record + { f = idʳ {a} A + ; f⁻¹ = λ {l} l∈A → l , l∈A , [] , lift refl , ++-identityʳ l + ; cong₁ = λ {l₁} {l₂} {l₁∈A} {l₂∈A} → idʳ-cong {a} A {l₁} {l₂} {l₁∈A} {l₂∈A} + ; cong₂ = λ l₁≈l₂ → l₁≈l₂ , lift _ + }) + } + where + open ≡.≡-Reasoning + + idˡ : ∀ {a aℓ} → + (A : Language (c ⊔ ℓ ⊔ a) aℓ) → + ∀ {l} → + l ∈ ((𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) ∙ A) → + l ∈ A + idˡ _ ([] , _ , l , l∈A , refl) = l∈A + + idˡ-cong : ∀ {a aℓ} → + (A : Language (c ⊔ ℓ ⊔ a) aℓ) → + ∀ {l₁ l₂ l₁∈A l₂∈A} → + ≈ᴸ ((𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝) ∙ A) {l₁} {l₂} l₁∈A l₂∈A → + ≈ᴸ A (idˡ {a} A l₁∈A) (idˡ {a} A l₂∈A) + idˡ-cong _ {l₁∈A = [] , _ , l₁ , l₁∈A , refl} {[] , _ , l₂ , l₂∈A , refl} (_ , l₁≈l₂) = l₁≈l₂ + + idʳ : ∀ {a aℓ} → + (A : Language (c ⊔ ℓ ⊔ a) aℓ) → + ∀ {l} → + l ∈ (A ∙ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)) → + l ∈ A + idʳ A (l , l∈A , [] , _ , refl) = ∈-cong A (sym (++-identityʳ l)) l∈A + + idʳ-cong : ∀ {a aℓ} → + (A : Language (c ⊔ ℓ ⊔ a) aℓ) → + ∀ {l₁ l₂ l₁∈A l₂∈A} → + ≈ᴸ (A ∙ (𝕃.Lift (ℓ ⊔ a) aℓ ｛ε｝)) {l₁} {l₂} l₁∈A l₂∈A → + ≈ᴸ A (idʳ {a} A l₁∈A) (idʳ {a} A l₂∈A) + idʳ-cong A {l₁∈A = l₁ , l₁∈A , [] , _ , refl} {l₂ , l₂∈A , [] , _ , refl} (l₁≈l₂ , _) = + ≈ᴸ-cong A (sym (++-identityʳ l₁)) (sym (++-identityʳ l₂)) l₁∈A l₂∈A l₁≈l₂ + +∙-monotone : ∀ {a aℓ b bℓ} → _∙_ Preserves₂ _≤_ {a} {aℓ} ⟶ _≤_ {b} {bℓ} ⟶ _≤_ +∙-monotone X≤Y U≤V = record + { f = λ {(_ , l₁∈X , _ , l₂∈U , l₁++l₂≡l) → -, X≤Y.f l₁∈X , -, U≤V.f l₂∈U , l₁++l₂≡l} + ; cong = Product.map X≤Y.cong U≤V.cong } + where + module X≤Y = _≤_ X≤Y + module U≤V = _≤_ U≤V diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda index daa1628..b06be3d 100644 --- a/src/Cfe/Language/Construct/Single.agda +++ b/src/Cfe/Language/Construct/Single.agda @@ -6,70 +6,23 @@ import Relation.Binary.PropositionalEquality as ≡ module Cfe.Language.Construct.Single {c ℓ} (over : Setoid c ℓ) - (≈-trans-bijₗ : ∀ {a b c b≈c} - → Bijective ≡._≡_ ≡._≡_ (flip (Setoid.trans over {a} {b} {c}) b≈c)) - (≈-trans-reflₗ : ∀ {a b a≈b} - → Setoid.trans over {a} a≈b (Setoid.refl over {b}) ≡.≡ a≈b) - (≈-trans-symₗ : ∀ {a b c a≈b a≈c b≈c} - → Setoid.trans over {a} {b} {c} a≈b b≈c ≡.≡ a≈c - → Setoid.trans over a≈c (Setoid.sym over b≈c) ≡.≡ a≈b) - (≈-trans-transₗ : ∀ {a b c d a≈b a≈c a≈d b≈c c≈d} - → Setoid.trans over {a} {b} a≈b b≈c ≡.≡ a≈c - → Setoid.trans over {a} {c} {d} a≈c c≈d ≡.≡ a≈d - → Setoid.trans over a≈b (Setoid.trans over b≈c c≈d) ≡.≡ a≈d) where open Setoid over renaming (Carrier to C) open import Cfe.Language over hiding (_≈_) open import Data.List -open import Data.List.Relation.Binary.Equality.Setoid over open import Data.Product as Product +open import Data.Unit open import Level -private - ∷-inj : {a b : C} {l₁ l₂ : List C} {a≈b a≈b′ : a ≈ b} {l₁≋l₂ l₁≋l₂′ : l₁ ≋ l₂} → ≡._≡_ {A = a ∷ l₁ ≋ b ∷ l₂} (a≈b ∷ l₁≋l₂) (a≈b′ ∷ l₁≋l₂′) → (a≈b ≡.≡ a≈b′) × (l₁≋l₂ ≡.≡ l₁≋l₂′) - ∷-inj ≡.refl = ≡.refl , ≡.refl - - ≋-trans-injₗ : {x l₁ l₂ : List C} → {l₁≋l₂ : l₁ ≋ l₂} → Injective ≡._≡_ ≡._≡_ (flip (≋-trans {x}) l₁≋l₂) - ≋-trans-injₗ {_} {_} {_} {_} {[]} {[]} _ = ≡.refl - ≋-trans-injₗ {_} {_} {_} {_ ∷ _} {_ ∷ _} {_ ∷ _} = uncurry (≡.cong₂ _∷_) - ∘ Product.map (proj₁ ≈-trans-bijₗ) ≋-trans-injₗ - ∘ ∷-inj - - ≋-trans-surₗ : {x l₁ l₂ : List C} → {l₁≋l₂ : l₁ ≋ l₂} → Surjective {A = x ≋ l₁} ≡._≡_ ≡._≡_ (flip (≋-trans {x}) l₁≋l₂) - ≋-trans-surₗ {_} {_} {_} {[]} [] = [] , ≡.refl - ≋-trans-surₗ {_} {_} {_} {_ ∷ _} (a≈c ∷ x≋l₂) = Product.zip _∷_ (≡.cong₂ _∷_) (proj₂ ≈-trans-bijₗ a≈c) (≋-trans-surₗ x≋l₂) - - ≋-trans-reflₗ : {l₁ l₂ : List C} {l₁≋l₂ : l₁ ≋ l₂} → ≋-trans l₁≋l₂ ≋-refl ≡.≡ l₁≋l₂ - ≋-trans-reflₗ {_} {_} {[]} = ≡.refl - ≋-trans-reflₗ {_} {_} {a≈b ∷ l₁≋l₂} = ≡.cong₂ _∷_ ≈-trans-reflₗ ≋-trans-reflₗ - - ≋-trans-symₗ : {l₁ l₂ l₃ : List C} {l₁≋l₂ : l₁ ≋ l₂} {l₁≋l₃ : l₁ ≋ l₃} {l₂≋l₃ : l₂ ≋ l₃} - → ≋-trans l₁≋l₂ l₂≋l₃ ≡.≡ l₁≋l₃ - → ≋-trans l₁≋l₃ (≋-sym l₂≋l₃) ≡.≡ l₁≋l₂ - ≋-trans-symₗ {_} {_} {_} {[]} {[]} {[]} _ = ≡.refl - ≋-trans-symₗ {_} {_} {_} {_ ∷ _} {_ ∷ _} {_ ∷ _} = uncurry (≡.cong₂ _∷_) - ∘ Product.map ≈-trans-symₗ ≋-trans-symₗ - ∘ ∷-inj - - ≋-trans-transₗ : {l₁ l₂ l₃ l₄ : List C} - → {l₁≋l₂ : l₁ ≋ l₂} {l₁≋l₃ : l₁ ≋ l₃} {l₁≋l₄ : l₁ ≋ l₄} {l₂≋l₃ : l₂ ≋ l₃} {l₃≋l₄ : l₃ ≋ l₄} - → ≋-trans l₁≋l₂ l₂≋l₃ ≡.≡ l₁≋l₃ - → ≋-trans l₁≋l₃ l₃≋l₄ ≡.≡ l₁≋l₄ - → ≋-trans l₁≋l₂ (≋-trans l₂≋l₃ l₃≋l₄) ≡.≡ l₁≋l₄ - ≋-trans-transₗ {l₁≋l₂ = []} {[]} {[]} {[]} {[]} _ _ = ≡.refl - ≋-trans-transₗ {l₁≋l₂ = _ ∷ _} {_ ∷ _} {_ ∷ _} {_ ∷ _} {_ ∷ _} = uncurry (≡.cong₂ _∷_) - ∘₂ uncurry (Product.zip ≈-trans-transₗ ≋-trans-transₗ) - ∘₂ curry (Product.map ∷-inj ∷-inj) - -｛_｝ : C → Language (c ⊔ ℓ) (c ⊔ ℓ) +｛_｝ : C → Language (c ⊔ ℓ) 0ℓ ｛ c ｝ = record - { Carrier = [ c ] ≋_ - ; _≈_ = λ l≋m l≋n → ∃[ m≋n ] ≋-trans l≋m m≋n ≡.≡ l≋n + { Carrier = λ l → ∃[ a ] (l ≡.≡ [ a ] × a ≈ c) + ; _≈_ = λ _ _ → ⊤ ; isEquivalence = record - { refl = ≋-refl , ≋-trans-reflₗ - ; sym = Product.map ≋-sym ≋-trans-symₗ - ; trans = Product.zip ≋-trans ≋-trans-transₗ + { refl = tt + ; sym = λ _ → tt + ; trans = λ _ _ → tt } } 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 -- cgit v1.2.3