upload GlobalBisim

formalizations/guarded-cubical/Semantics/GlobalBisim.agda

+{-# OPTIONS --rewriting --guarded #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+module Semantics.GlobalBisim where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Function
+open import Cubical.Data.Sigma
+open import Cubical.Data.Nat hiding (_^_)
+open import Cubical.Data.Sum
+
+open import Cubical.Data.Empty as ⊥
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Order.Poset
+
+open import Cubical.HITs.PropositionalTruncation renaming (elim to PTelim ; rec to PTrec)
+
+open import Common.Common
+open import Common.Later
+open import Common.LaterProperties
+open import Common.ClockProperties
+open import Semantics.Lift 
+open import Semantics.WeakBisimilarity
+open import Semantics.GlobalLift
+
+
+private
+  variable
+    ℓ ℓ' ℓR : Level
+
+
+-- module WBSum {ℓ ℓR : Level} (X : Type ℓ) (R : X -> X -> Type ℓR) (k : Clock) = BisimSum k X R
+
+module GlobalBisimSum  (X : Type ℓ) (R : X -> X -> Type ℓR) where
+  -- open WBSum X R
+  --open module WBSum = BisimSum X R -- enaming (_≈_ to _≈S_)
+
+  --_≈[_]_ : {!L k X → (k : Clock) → L k X!}
+  --l ≈[ k ] l' = {!_≈_ k l l'!}
+
+  ≈S : (k : Clock) → L k X → L k X → Type (ℓ-max ℓ ℓR)
+  ≈S k = BisimSum._≈_ k X R
+  syntax ≈S k x y = x ≈[ k ] y
+
+  _≈g_ : L^gl X -> L^gl X -> Type (ℓ-max ℓ ℓR)
+  l1 ≈g l2 = ∀ k → (l1 k) ≈[ k ] (l2 k)
+
+  case1 : (l l' : L^gl X) -> Type (ℓ-max ℓ ℓR)
+  case1 l l' = Σ[ x ∈ X ] Σ[ y ∈ X ] (l ≡ ηL^gl x) × (l' ≡ ηL^gl y) × R x y
+
+  case2 : (l l' : L^gl X) -> Type (ℓ-max ℓ ℓR)
+  case2 l l' =
+    Σ[ x ∈ X ] ((l  ≡ ηL^gl x)
+      × ∥ Σ[ n ∈ ℕ ] Σ[ y ∈ X ] ((l' ≡ (δL^gl ^ n) (ηL^gl y)) × R x y) ∥₁)
+
+  case3 : (l l' : L^gl X) -> Type (ℓ-max ℓ ℓR)
+  case3 l l' =
+    Σ[ y ∈ X ] ((l' ≡ ηL^gl y)
+      × ∥ Σ[ n ∈ ℕ ] Σ[ x ∈ X ] ((l  ≡ (δL^gl ^ n) (ηL^gl x)) × R x y) ∥₁)
+
+  case4 : (l l' : L^gl X) -> Type (ℓ-max ℓ ℓR)
+  case4 l l' = Σ[ lx~ ∈ (∀ k -> ▹ k , L k X) ] Σ[ ly~ ∈ (∀ k -> ▹ k , (L^gl X)) ]
+    (l ≡ λ k → lx~ k {!!}) × (l' ≡ {!!}) × (▸ (λ t -> {!!}))
+
+  _≈g'_ : {!!}
+  l1 ≈g' l2 = {!!}
+
+  L^gl-R-iso : clock-irrel X -> (l l' : L^gl X) ->
+    Iso (l ≈g l') (case1 l l' ⊎ (case2 l l' ⊎ (case3 l l' ⊎ case4 l l'))) 
+  L^gl-R-iso X-irrel l l' =
+    (l ≈g l')
+      Iso⟨ {!!} ⟩
+      {!!} Iso⟨ {!!} ⟩ {!!}
+    (case1 l l' ⊎ (case2 l l' ⊎ (case3 l l' ⊎ case4 l l'))) ∎Iso
+  
+      
+  
+