From ff3600687249a19ae63353f7791b137094f5a5a1 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 18 Feb 2021 19:04:09 +0000
Subject: Another redefinition of Language.

---
 src/Cfe/Language/Construct/Union.agda | 99 ++++++++++-------------------------
 1 file changed, 28 insertions(+), 71 deletions(-)

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

diff --git a/src/Cfe/Language/Construct/Union.agda b/src/Cfe/Language/Construct/Union.agda
index 44d4c3f..ee8b0f7 100644
--- a/src/Cfe/Language/Construct/Union.agda
+++ b/src/Cfe/Language/Construct/Union.agda
@@ -4,99 +4,56 @@ open import Relation.Binary
 import Cfe.Language
 
 module Cfe.Language.Construct.Union
-  {c ℓ a aℓ b bℓ} (setoid : Setoid c ℓ)
-  (A : Cfe.Language.Language setoid a aℓ)
-  (B : Cfe.Language.Language setoid b bℓ)
+  {c ℓ a aℓ b bℓ} (over : Setoid c ℓ)
+  (A : Cfe.Language.Language over a aℓ)
+  (B : Cfe.Language.Language over b bℓ)
   where
 
 open import Data.Empty
 open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid setoid
+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 setoid
-open Language
+open import Cfe.Language over hiding (Lift)
 
-open Setoid setoid renaming (Carrier to C)
+open Setoid over renaming (Carrier to C)
 
 infix 4 _≈ᵁ_
 infix 4 _∪_
 
 Union : List C → Set (a ⊔ b)
-Union l = 𝕃 A l ⊎ 𝕃 B l
+Union l = l ∈ A ⊎ l ∈ B
 
-_≈ᵁ_ : {l : List C} → Rel (Union l) (aℓ ⊔ bℓ)
-(inj₁ x) ≈ᵁ (inj₁ y) = Lift bℓ (_≈ᴸ_ A x y)
+_≈ᵁ_ : {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)
-
-⤖ᵁ : {l₁ l₂ : List C} → l₁ ≋ l₂ → Union l₁ → Union l₂
-⤖ᵁ l₁≋l₂ = Sum.map (⤖ A l₁≋l₂) (⤖ B l₁≋l₂)
+(inj₂ x) ≈ᵁ (inj₂ y) = Lift aℓ (≈ᴸ B x y)
 
 _∪_ : Language (a ⊔ b) (aℓ ⊔ bℓ)
 _∪_ = record
-  { 𝕃 = Union
-  ; _≈ᴸ_ = _≈ᵁ_
-  ; ⤖ = ⤖ᵁ
-  ; isLanguage = record
-    { ≈ᴸ-isEquivalence = record
-      { refl = λ {x} → case x return (λ x → _≈ᵁ_ x x) of λ
-        { (inj₁ x) → lift (≈ᴸ-refl A)
-        ; (inj₂ y) → lift (≈ᴸ-refl B)
-        }
-      ; 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)
-          }
-      ; trans = λ {i} {j} {k} i≈ᵁj j≈ᵁk →
-        case ∃[ i ](∃[ j ](∃[ k ](i ≈ᵁ j × j ≈ᵁ k))) ∋ i , j , k , i≈ᵁj , j≈ᵁk
-        return (λ (i , _ , k , _) → i ≈ᵁ k) 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)
-          }
-      }
-    ; ⤖-cong = λ {_} {_} {l₁≋l₂} {x} {y} x≈ᵁy →
-      case ∃[ x ](∃[ y ](x ≈ᵁ y)) ∋ x , y , x≈ᵁy
-      return (λ (x , y , _) → (_≈ᵁ_ on ⤖ᵁ l₁≋l₂) x y) of λ
-        { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (⤖-cong A x≈ᵁy)
-        ; (inj₂ x , inj₂ y , lift x≈ᵁy) → lift (⤖-cong B x≈ᵁy)
-        }
-    ; ⤖-bijective = λ {_} {_} {l₁≋l₂} →
-      ( λ {x} {y} x≈ᵁy →
-        case ∃[ x ](∃[ y ]((_≈ᵁ_ on ⤖ᵁ l₁≋l₂) x y)) ∋ x , y , x≈ᵁy
-        return (λ (x , y , _) → x ≈ᵁ y) of λ
-          { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (⤖-injective A x≈ᵁy)
-          ; (inj₂ x , inj₂ y , lift x≈ᵁy) → lift (⤖-injective B x≈ᵁy)
-          })
-    , ( λ
-        { (inj₁ x) → Product.map inj₁ lift (⤖-surjective A x)
-        ; (inj₂ x) → Product.map inj₂ lift (⤖-surjective B x)
-        })
-    ; ⤖-refl = λ {_} {x} → case x return (λ x → ⤖ᵁ ≋-refl x ≈ᵁ x) of λ
-      { (inj₁ x) → lift (⤖-refl A)
-      ; (inj₂ y) → lift (⤖-refl B)
+  { Carrier = Union
+  ; _≈_ = _≈ᵁ_
+  ; isEquivalence = record
+    { refl = λ {_} {x} → case x return (λ x → x ≈ᵁ x) of λ
+      { (inj₁ x) → lift (≈ᴸ-refl A)
+      ; (inj₂ y) → lift (≈ᴸ-refl B)
       }
-    ; ⤖-sym = λ {_} {_} {x} {y} {l₁≋l₂} x≈ᵁy →
-      case ∃[ x ](∃[ y ](⤖ᵁ l₁≋l₂ x ≈ᵁ y)) ∋ x , y , x≈ᵁy
-      return (λ (x , y , _) → ⤖ᵁ (≋-sym l₁≋l₂) y ≈ᵁ x) of λ
-        { (inj₁ x , inj₁ y , lift x≈ᵁy) → lift (⤖-sym A x≈ᵁy)
-        ; (inj₂ x , inj₂ y , lift x≈ᵁy) → lift (⤖-sym 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)
         }
-    ; ⤖-trans = λ {_} {_} {_} {x} {y} {z} {l₁≋l₂} {l₂≋l₃} x≈ᵁy y≈ᵁz →
-      case (∃[ x ](∃[ y ](∃[ z ]((⤖ᵁ l₁≋l₂ x ≈ᵁ y) × (⤖ᵁ l₂≋l₃ y ≈ᵁ z))))) ∋
-           x , y , z , x≈ᵁy , y≈ᵁz
-      return (λ (x , _ , z , _ , _) → ⤖ᵁ (≋-trans l₁≋l₂ l₂≋l₃) x ≈ᵁ z) of λ
-        { (inj₁ x , inj₁ y , inj₁ z , lift x≈ᵁy , lift y≈ᵁz) →
-          lift (⤖-trans A x≈ᵁy y≈ᵁz)
-        ; (inj₂ x , inj₂ y , inj₂ z , lift x≈ᵁy , lift y≈ᵁz) →
-          lift (⤖-trans B x≈ᵁy y≈ᵁz)
+    ; 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)
         }
     }
   }
-- 
cgit v1.2.3