3 files changed, 189 insertions, 112 deletions
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