Move global lift code into separate file

formalizations/guarded-cubical/Results/IntensionalAdequacy.agda

@@ -17,6 +17,7 @@ open import Cubical.Foundations.Structure
 open import Cubical.Data.Empty.Base renaming (rec to exFalso)
 open import Cubical.Data.Sum
 open import Cubical.Data.Sigma
+open import Cubical.Data.Bool hiding (_≤_)
 open import Cubical.Relation.Nullary
 open import Cubical.Data.Unit renaming (Unit to ⊤)
 
@@ -25,13 +26,18 @@ open import Cubical.Foundations.Univalence
 
 open import Cubical.Foundations.Function
 
+open import Agda.Builtin.Equality renaming (_≡_ to _≣_) hiding (refl)
+open import Agda.Builtin.Equality.Rewrite
+
 import Semantics.StrongBisimulation
 import Semantics.Monotone.Base
-import Syntax.GradualSTLC
+-- import Syntax.GradualSTLC
 
 open import Common.Common
 open import Semantics.Predomains
 open import Semantics.Lift
+open import Semantics.Global
+
 
 -- TODO move definition of Predomain to a module that
 -- isn't parameterized by a clock!
@@ -45,152 +51,6 @@ private
 open Semantics.StrongBisimulation
 -- open StrongBisimulation.LiftPredomain
 
-
--- "Global" definitions
-L℧F : (X : Type) -> Type
-L℧F X = ∀ (k : Clock) -> L℧ k X
-
-ηF : {X : Type} -> X -> L℧F X
-ηF {X} x = λ k → η x
-
-℧F : {X : Type} -> L℧F X
-℧F = λ k -> ℧
-
-θF : {X : Type} -> L℧F X -> L℧F X
-θF lx = λ k → θ (λ t → lx k)
-
-δ-gl : {X : Type} -> L℧F X -> L℧F X
-δ-gl lx = λ k → δ k (lx k)
-
-δ-gl^n : (lxF : L℧F Nat) -> (n : Nat) -> (k : Clock) ->
-      ((δ-gl) ^ n) lxF k ≡ ((δ k) ^ n) (lxF k)
-δ-gl^n lxF zero k = refl
-δ-gl^n lxF (suc n') k = cong (δ k) (δ-gl^n lxF n' k)
-
-
-{-
- _Iso⟨_⟩_  : {ℓ ℓ' ℓ'' : Level} {B : Type ℓ'} {C : Type ℓ''}
-              (X : Type ℓ) →
-              Iso X B → Iso B C → Iso X C
-  _∎Iso     : {ℓ : Level} (A : Type ℓ) → Iso A A
-
-
-   Σ-Π-Iso   : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : A → Type ℓ'}
-              {C : (a : A) → B a → Type ℓ''} →
-              Iso ((a : A) → Σ-syntax (B a) (C a))
-                  (Σ-syntax ((a : A) → B a) (λ f → (a : A) → C a (f a)))
-
-   codomainIsoDep
-            : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : A → Type ℓ'}
-              {C : A → Type ℓ''} →
-              ((a : A) → Iso (B a) (C a)) → Iso ((a : A) → B a) ((a : A) → C a)
-
-   ⊎Iso      : {A.ℓa : Level} {A : Type A.ℓa} {C.ℓc : Level}
-              {C : Type C.ℓc} {B.ℓb : Level} {B : Type B.ℓb} {D.ℓd : Level}
-              {D : Type D.ℓd} →
-              Iso A C → Iso B D → Iso (A ⊎ B) (C ⊎ D)
--}
-
-Unit-clock-irrel : clock-irrel Unit
-Unit-clock-irrel M k k' with M k | M k'
-...  | tt | tt = refl
-
-∀kL℧-▹-Iso : {X : Type} -> Iso ((k : Clock) -> ▹_,_ k (L℧ k X)) ((k : Clock) -> L℧ k X) 
-∀kL℧-▹-Iso = force-iso
-
-∀clock-Σ : {A : Type} -> {B : A -> Clock -> Type} ->
-    -- (∀ a k -> clock-irrel (B a k)) ->
-    clock-irrel A ->
-    (∀ (k : Clock) -> Σ A (λ a -> B a k)) ->
-    Σ A (λ a -> ∀ (k : Clock) -> B a k)
-∀clock-Σ {A} {B} H-clk-irrel H =
-    let a = fst (H k0) in
-      a , (λ k -> transport
-                   (λ i → B (H-clk-irrel (fst ∘ H) k k0 i) k)
-                   (snd (H k)))
-  -- NTS:  B (fst (H k)) k ≡ B (fst (H k0)) k
-  -- i.e. essentially need to show that fst (H k) ≡ fst (H k0)
-  -- This follows from clock irrelevance for A, with M = fst ∘ H of type Clock -> A
-
-
-
-Iso-Π-⊎ : {A B : Clock -> Type} ->
-  Iso ((k : Clock) -> (A k ⊎ B k)) (((k : Clock) -> A k) ⊎ ((k : Clock) -> B k))
-Iso-Π-⊎ {A} {B} = iso to inv sec retr
-  where
-    to : ((k : Clock) → A k ⊎ B k) → ((k : Clock) → A k) ⊎ ((k : Clock) → B k)
-    to f with f k0
-    ... | inl a = inl (λ k → transport (type-clock-irrel A k0 k) a)
-    ... | inr b = inr (λ k → transport (type-clock-irrel B k0 k) b)
-
-    inv : ((k : Clock) → A k) ⊎ ((k : Clock) → B k) -> ((k : Clock) → A k ⊎ B k)
-    inv (inl f) k = inl (f k)
-    inv (inr f) k = inr (f k)
-
-    sec : section to inv
-    sec (inl f) = cong inl (clock-ext λ k -> {!!})
-    sec (inr f) = cong inr (clock-ext (λ k -> {!!}))
-
-    retr : retract to inv
-    retr f with (f k0)
-    ... | inl a = clock-ext (λ k → {!!})
-    ... | inr b = {!!}
-
-  {-
-  transport-filler
-            : {ℓ : Level} {A B : Type ℓ} (p : A ≡ B) (x : A) →
-              PathP (λ i → p i) x (transport p x)
-  -}              
-
-L℧-iso : {k : Clock} -> {X : Type} -> Iso (L℧ k X) ((X ⊎ ⊤) ⊎ (▹_,_ k (L℧ k X)))
-L℧-iso {k} {X} = iso f g sec retr
-  where
-    f : L℧ k X → (X ⊎ ⊤) ⊎ (▹ k , L℧ k X)
-    f (η x) = inl (inl x)
-    f ℧ = inl (inr tt)
-    f (θ lx~) = inr lx~
-
-    g : (X ⊎ ⊤) ⊎ (▹ k , L℧ k X) -> L℧ k X
-    g (inl (inl x)) = η x
-    g (inl (inr tt)) = ℧
-    g (inr lx~) = θ lx~
-
-    sec : section f g
-    sec (inl (inl x)) = refl
-    sec (inl (inr tt)) = refl
-    sec (inr lx~) = refl
-
-    retr : retract f g
-    retr (η x) = refl
-    retr ℧ = refl
-    retr (θ x) = refl
-
-
-L℧F-iso : {X : Type} -> clock-irrel X -> Iso (L℧F X) ((X ⊎ ⊤) ⊎ (L℧F X))
-L℧F-iso {X} H-irrel-X =
-  (∀ k -> L℧ k X)
-
-          Iso⟨ codomainIsoDep (λ k -> L℧-iso) ⟩
-  
-  (∀ k -> (X ⊎ ⊤) ⊎ (▹_,_ k (L℧ k X)))
-
-          Iso⟨ Iso-Π-⊎ ⟩
-
-  (∀ (k : Clock) -> (X ⊎ ⊤)) ⊎ (∀ k -> ▹_,_ k (L℧ k X))
-
-          Iso⟨ ⊎Iso Iso-Π-⊎ idIso ⟩
-  
-  ((∀ (k : Clock) -> X) ⊎ (∀ (k : Clock) -> ⊤)) ⊎
-       (∀ k -> ▹_,_ k (L℧ k X))
-       
-          Iso⟨ ⊎Iso (⊎Iso (Iso-∀kA-A H-irrel-X) (Iso-∀kA-A Unit-clock-irrel)) force-iso ⟩
-                    
-  (X ⊎ ⊤) ⊎ (L℧F X) ∎Iso
-
-
-unfold-L℧F : {X : Type} -> clock-irrel X -> (L℧F X) ≡ ((X ⊎ ⊤) ⊎ (L℧F X))
-unfold-L℧F H = ua (isoToEquiv (L℧F-iso H))
-
    
 
 -- Adequacy of lock-step relation
@@ -204,19 +64,15 @@ module AdequacyLockstep
   _≾-gl_ : {p : Predomain} -> (L℧F ⟨ p ⟩) -> (L℧F ⟨ p ⟩) -> Type
   _≾-gl_ {p} lx ly = ∀ (k : Clock) -> _≾_ k p (lx k) (ly k)
 
-  -- _≾'_ : {k : Clock} -> L℧ k Nat → L℧ k Nat → Type
-  -- _≾'_ {k} = {!!}
-
-
   -- These should probably be moved to the module where _≾'_ is defined.
   ≾'-℧ : {k : Clock} -> (lx : L℧ k Nat) ->
-    _≾'_ k (ℕ k0) lx ℧ -> lx ≡ ℧
+    _≾'_ k ℕ lx ℧ -> lx ≡ ℧
   ≾'-℧ (η x) ()
   ≾'-℧ ℧ _ = refl
   ≾'-℧ (θ x) ()
 
   ≾'-θ : {k : Clock} -> (lx : L℧ k Nat) -> (ly~ : ▹_,_ k (L℧ k Nat)) ->
-    _≾'_ k (ℕ k0) lx (θ ly~) ->
+    _≾'_ k ℕ lx (θ ly~) ->
     Σ (▹_,_ k (L℧ k Nat)) (λ lx~ -> lx ≡ θ lx~)
   ≾'-θ (θ lz~) ly~ H = lz~ , refl
   ≾'-θ ℧ ly~ x = {!!}
@@ -237,9 +93,9 @@ module AdequacyLockstep
   adequate-err' :
     (m : Nat) ->
     (lxF : L℧F Nat) ->
-    (H-lx : _≾-gl_ {ℕ k0} lxF ((δ-gl ^ m) ℧F)) ->
+    (H-lx : _≾-gl_ {ℕ} lxF ((δ-gl ^ m) ℧F)) ->
     (Σ (Nat) λ n -> (n ≤ m) × ((lxF ≡ (δ-gl ^ n) ℧F)))
-  adequate-err' zero lxF H-lx with (Iso.fun (L℧F-iso nat-clock-irrel) lxF)
+  adequate-err' zero lxF H-lx with (Iso.fun (L℧F-iso-irrel nat-clock-irrel) lxF)
   ... | inl (inl x) = zero , {!!}
   ... | _ = {!!}
   adequate-err' (suc m) = {!!}
@@ -247,10 +103,10 @@ module AdequacyLockstep
   adequate-err :
     (m : Nat) ->
     (lxF : L℧F Nat) ->
-    (H-lx : _≾-gl_ {ℕ k0} lxF ((δ-gl ^ m) ℧F)) ->
+    (H-lx : _≾-gl_ {ℕ} lxF ((δ-gl ^ m) ℧F)) ->
     (Σ (Nat) λ n -> (n ≤ m) × ((lxF ≡ (δ-gl ^ n) ℧F)))
   adequate-err zero lxF H-lxF =
-    let H' = transport (λ i -> ∀ k -> unfold-≾ k (ℕ k0) i (lxF k) (℧F k)) H-lxF in
+    let H' = transport (λ i -> ∀ k -> unfold-≾ k (ℕ) i (lxF k) (℧F k)) H-lxF in
         zero , ≤-refl , clock-ext λ k → ≾'-℧ (lxF k) (H' k)
            -- H' says that for all k, (lxF k) ≾' (℧F k) i.e.
            -- for all k, (lxF k) ≾' ℧, which means, by definition of ≾',
@@ -263,10 +119,10 @@ module AdequacyLockstep
         aux : (k : Clock) -> (Σ (▹ k , L℧ k Nat) (λ lx~ → lxF k ≡ θ lx~)) × _
         aux k =  let RHS = (((δ-gl ^ m') ℧F) k) in
                  let RHS' = (δ k RHS) in
-                 let H1 = transport (λ i -> unfold-≾ k (ℕ k0) i (lxF k) RHS') (H-lxF k) in
+                 let H1 = transport (λ i -> unfold-≾ k (ℕ) i (lxF k) RHS') (H-lxF k) in
                  let pair = ≾'-θ (lxF k) (next RHS) H1 in 
-                 let H2 = transport (λ i → _≾'_ k (ℕ k0) (snd pair i) RHS') H1 in
-                 let H3 = transport ((λ i -> (t : Tick k) -> _≾_ k (ℕ k0) (tick-irrelevance (fst pair) t ◇ i) RHS)) H2 in
+                 let H2 = transport (λ i → _≾'_ k (ℕ) (snd pair i) RHS') H1 in
+                 let H3 = transport ((λ i -> (t : Tick k) -> _≾_ k (ℕ) (tick-irrelevance (fst pair) t ◇ i) RHS)) H2 in
                  pair , (H3 ◇)
        
 
@@ -289,9 +145,6 @@ module AdequacyLockstep
 
 
 
-
-
-
 module AdequacyBisim where
 
   open Semantics.StrongBisimulation
@@ -331,7 +184,7 @@ module AdequacyBisim where
         H' = {!!}
     
 
-  open GlobalBisim (ℕ k0)
+  open GlobalBisim (ℕ)
 
 
 
@@ -343,11 +196,11 @@ module AdequacyBisim where
     (Σ (Nat) λ n -> ((lxF ≡ (δ-gl ^ n) ℧F)))
   adequate-err zero lxF H-lx = (fst H3) , clock-ext (snd H4)
     where
-      H1 : (k : Clock) -> _≈'_ k (ℕ k0) (next (_≈_ k (ℕ k0))) (lxF k) (℧F k)
-      H1 = transport (λ i → ∀ k -> unfold-≈ k (ℕ k0) i (lxF k) (℧F k)) H-lx
+      H1 : (k : Clock) -> _≈'_ k (ℕ) (next (_≈_ k (ℕ))) (lxF k) (℧F k)
+      H1 = transport (λ i → ∀ k -> unfold-≈ k (ℕ) i (lxF k) (℧F k)) H-lx
 
       H2 : (k : Clock) -> Σ Nat (λ n → lxF k ≡ (δ k ^ n) ℧)
-      H2 k = ≈-℧ k (ℕ k0) (lxF k) (H1 k)
+      H2 k = ≈-℧ k (ℕ) (lxF k) (H1 k)
 
       H3 : Σ Nat (λ n -> ∀ (k : Clock) -> lxF k ≡ (δ k ^ n) ℧)
       H3 = ∀clock-Σ nat-clock-irrel H2
@@ -361,3 +214,36 @@ module AdequacyBisim where
      
   adequate-err (suc m') lxF H-lx = {!!}
 
+
+
+module DynExp where
+
+  open import Semantics.SemanticsNew
+  open import Semantics.PredomainInternalHom
+  open import Semantics.StrongBisimulation
+  open LiftPredomain
+  open import Semantics.Monotone.Base
+  open import Semantics.Monotone.MonFunCombinators
+  open import Cubical.Relation.Binary.Poset
+  open import Semantics.Predomains
+
+
+  DynUnfold : Iso
+    (∀ k -> ⟨ DynP k ⟩)
+    (Nat ⊎ (∀ k -> ⟨ DynP k ==> 𝕃 k (DynP k) ⟩))
+  DynUnfold = {!!}
+
+
+  dyn-clk : (k k' : Clock) -> ⟨ DynP k ==> DynP k' ⟩
+  dyn-clk = {!!}
+
+
+  𝔽𝕃 : (Clock -> Predomain) -> Predomain
+  𝔽𝕃 f = 𝔽 (λ k → 𝕃 k (f k))
+
+  dyn-eqn : Iso
+    ⟨ (ℕ ⊎d (𝔽 (λ k -> DynP k ==> 𝕃 k (DynP k) ))) ⟩
+    ⟨ (ℕ ⊎d (𝔽 DynP)) ==> 𝔽𝕃 DynP ⟩
+  dyn-eqn = {!!}
+    
+

formalizations/guarded-cubical/Semantics/Global.agda

+{-# OPTIONS --cubical --rewriting --guarded #-}
+{-# OPTIONS --guardedness #-}
+
+ -- to allow opening this module in other files while there are still holes
+{-# OPTIONS --allow-unsolved-metas #-}
+
+
+open import Common.Later
+
+module Semantics.Global where
+
+
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat renaming (ℕ to Nat) hiding (_·_ ; _^_)
+open import Cubical.Data.Nat.Order
+open import Cubical.Foundations.Structure
+open import Cubical.Data.Empty.Base renaming (rec to exFalso)
+open import Cubical.Data.Sum
+open import Cubical.Data.Sigma
+open import Cubical.Data.Bool hiding (_≤_)
+open import Cubical.Relation.Nullary
+open import Cubical.Data.Unit renaming (Unit to ⊤)
+
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+
+open import Cubical.Foundations.Function
+
+open import Agda.Builtin.Equality renaming (_≡_ to _≣_) hiding (refl)
+open import Agda.Builtin.Equality.Rewrite
+
+import Semantics.StrongBisimulation
+import Semantics.Monotone.Base
+-- import Syntax.GradualSTLC
+
+open import Common.Common
+open import Semantics.Predomains
+open import Semantics.Lift
+
+-- TODO move definition of Predomain to a module that
+-- isn't parameterized by a clock!
+
+private
+  variable
+    l : Level
+    X : Type l
+
+-- Lift monad
+open Semantics.StrongBisimulation
+-- open StrongBisimulation.LiftPredomain
+
+-- "Global" definitions
+-- TODO in the general setting, X should have type Clock -> Type
+-- and L℧F X should be equal to ∀ k -> L℧ k (X k)
+L℧F : (X : Type) -> Type
+L℧F X = ∀ (k : Clock) -> L℧ k X
+
+□ : Type -> Type
+□ X = ∀ (k : Clock) -> X
+
+ηF : {X : Type} -> □ X -> L℧F X
+ηF {X} x = λ k → η (x k)
+
+℧F : {X : Type} -> L℧F X
+℧F = λ k -> ℧
+
+θF : {X : Type} -> L℧F X -> L℧F X
+θF lx = λ k → θ (λ t → lx k)
+
+δ-gl : {X : Type} -> L℧F X -> L℧F X
+δ-gl lx = λ k → δ k (lx k)
+
+δ-gl^n : {X : Type} (lxF : L℧F X) -> (n : Nat) -> (k : Clock) ->
+      ((δ-gl) ^ n) lxF k ≡ ((δ k) ^ n) (lxF k)
+δ-gl^n lxF zero k = refl
+δ-gl^n lxF (suc n') k = cong (δ k) (δ-gl^n lxF n' k)
+
+
+
+{- Iso definitions used in this file:
+
+ _Iso⟨_⟩_  : {ℓ ℓ' ℓ'' : Level} {B : Type ℓ'} {C : Type ℓ''}
+              (X : Type ℓ) →
+              Iso X B → Iso B C → Iso X C
+  _∎Iso     : {ℓ : Level} (A : Type ℓ) → Iso A A
+
+
+   Σ-Π-Iso   : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : A → Type ℓ'}
+              {C : (a : A) → B a → Type ℓ''} →
+              Iso ((a : A) → Σ-syntax (B a) (C a))
+                  (Σ-syntax ((a : A) → B a) (λ f → (a : A) → C a (f a)))
+
+   codomainIsoDep
+            : {ℓ ℓ' ℓ'' : Level} {A : Type ℓ} {B : A → Type ℓ'}
+              {C : A → Type ℓ''} →
+              ((a : A) → Iso (B a) (C a)) → Iso ((a : A) → B a) ((a : A) → C a)
+
+   ⊎Iso      : {A.ℓa : Level} {A : Type A.ℓa} {C.ℓc : Level}
+              {C : Type C.ℓc} {B.ℓb : Level} {B : Type B.ℓb} {D.ℓd : Level}
+              {D : Type D.ℓd} →
+              Iso A C → Iso B D → Iso (A ⊎ B) (C ⊎ D)
+
+  Σ-cong-iso-fst
+            : {A.ℓ : Level} {A : Type A.ℓ} {B..1 : Level} {A' : Type B..1}
+              {B.ℓ : Level} {B : A' → Type B.ℓ} (isom : Iso A A') →
+              Iso (Σ A (B ∘ Iso.fun isom)) (Σ A' B)
+
+  Σ-cong-iso-snd
+            : {B'..1 : Level} {A : Type B'..1} {B.ℓ : Level} {B : A → Type B.ℓ}
+              {B'.ℓ : Level} {B' : A → Type B'.ℓ} →
+              ((x : A) → Iso (B x) (B' x)) → Iso (Σ A B) (Σ A B')
+
+-}
+
+
+
+Unit-clock-irrel : clock-irrel Unit
+Unit-clock-irrel M k k' with M k | M k'
+...  | tt | tt = refl
+
+∀kL℧-▹-Iso : {X : Type} -> Iso
+  ((k : Clock) -> ▹_,_ k (L℧ k X))
+  ((k : Clock) -> L℧ k X) 
+∀kL℧-▹-Iso = force-iso
+
+
+bool2ty : Type -> Type -> Bool -> Type
+bool2ty A B true = A
+bool2ty A B false = B
+
+bool2ty-eq : {X : Type} {A B : X -> Type} ->
+  (b : Bool) ->
+  (∀ (x : X) -> bool2ty (A x) (B x) b) ≡
+  bool2ty (∀ x -> A x) (∀ x -> B x) b
+bool2ty-eq {X} {A} {B} true = refl
+bool2ty-eq {X} {A} {B} false = refl
+
+
+
+Iso-⊎-ΣBool : {A B : Type} -> Iso (A ⊎ B) (Σ Bool (λ b -> bool2ty A B b))
+Iso-⊎-ΣBool {A} {B} = iso to inv sec retr
+  where
+    to : A ⊎ B → Σ Bool (λ b -> bool2ty A B b)
+    to (inl a) = true , a
+    to (inr b) = false , b
+
+    inv : Σ Bool (bool2ty A B) → A ⊎ B
+    inv (true , a) = inl a
+    inv (false , b) = inr b
+
+    sec : section to inv
+    sec (true , a) = refl
+    sec (false , b) = refl
+
+    retr : retract to inv
+    retr (inl a) = refl
+    retr (inr b) = refl
+
+
+
+∀clock-Σ : {A : Type} -> {B : A -> Clock -> Type} ->
+    clock-irrel A ->
+    (∀ (k : Clock) -> Σ A (λ a -> B a k)) ->
+    Σ A (λ a -> ∀ (k : Clock) -> B a k)
+∀clock-Σ {A} {B} H-clk-irrel p =
+    let a = fst (p k0) in
+      a , (λ k -> transport
+                   (λ i → B (H-clk-irrel (fst ∘ p) k k0 i) k)
+                   (snd (p k)))
+  -- NTS:  B (fst (p k)) k ≡ B (fst (p k0)) k
+  -- i.e. essentially need to show that fst (p k) ≡ fst (p k0)
+  -- This follows from clock irrelevance for A, with M = fst ∘ p of type Clock -> A
+
+
+
+
+MLTT-choice : {S : Type} -> {A : S -> Type} -> {B : (s : S) -> A s -> Type} ->
+  Iso (∀ (s : S) -> (Σ[ x ∈ A s ] B s x))
+      (Σ[ x ∈ (∀ s -> A s) ] ( ∀ s -> B s (x s) ))
+MLTT-choice = Σ-Π-Iso
+
+Eq-Iso : {A B : Type} ->
+  A ≡ B -> Iso A B
+Eq-Iso {A} {B} H-eq = subst (Iso A) H-eq idIso
+-- same as: transport (cong (Iso A) H-eq) idIso
+
+
+
+Iso-∀clock-Σ : {A : Type} -> {B : A -> Clock -> Type} ->
+  clock-irrel A ->
+  Iso
+    (∀ (k : Clock) -> Σ A (λ a -> B a k))
+    (Σ A (λ a -> ∀ (k : Clock) -> B a k))
+Iso-∀clock-Σ {A} {B} H-clk-irrel =
+  (∀ (k : Clock) -> Σ A (λ a -> B a k))
+     Iso⟨ Σ-Π-Iso {A = Clock} {B = λ _ -> A} {C = λ k a -> B a k} ⟩
+     
+  (Σ ((k : Clock) → A) (λ f → (k : Clock) → B (f k) k))
+     Iso⟨ ( Σ-cong-iso-snd (λ f → codomainIsoDep (λ k → Eq-Iso (λ i → B (H-clk-irrel f k k0 i) k)))) ⟩
+
+  (Σ ((k : Clock) → A) (λ f → (k : Clock) → B (f k0) k))
+     Iso⟨ Σ-cong-iso-fst {B = λ a -> ∀ k' -> B a k'} (Iso-∀kA-A H-clk-irrel) ⟩
+     
+  (Σ A (λ a -> ∀ (k : Clock) -> B a k)) ∎Iso
+
+-- Action of the above isomorphism
+Iso-∀clock-Σ-fun : {A : Type} {B : A -> Clock -> Type} ->
+  (H : clock-irrel A) ->
+  (f : (k : Clock) -> Σ A (λ a -> B a k)) ->
+  Iso.fun (Iso-∀clock-Σ {A} {B} H) f ≡ (fst (f k0) , {!!})
+Iso-∀clock-Σ-fun {A} {B} H f = {!!}
+
+{- Note:
+          Σ-cong-iso-fst
+            : {A.ℓ : Level} {A : Type A.ℓ} {B..1 : Level} {A' : Type B..1}
+              {B.ℓ : Level} {B : A' → Type B.ℓ} (isom : Iso A A') →
+              Iso (Σ A (B ∘ Iso.fun isom)) (Σ A' B)
+
+    In this case, the isomorphism function associated with Iso-∀kA-A
+    takes f : (∀ (k : Clock) -> A) to A by applying f to k0.
+    This is why we need the intermediate step of transforming B (f k) k
+    into B (f k0) k.
+
+-}
+
+
+
+Iso-Π-⊎-clk : {A B : Clock -> Type} ->
+  Iso
+    ((k : Clock) -> (A k ⊎ B k))
+    (((k : Clock) -> A k) ⊎ ((k : Clock) -> B k))
+Iso-Π-⊎-clk {A} {B} =
+  (∀ (k : Clock) -> (A k ⊎ B k))
+    Iso⟨ codomainIsoDep (λ k -> Iso-⊎-ΣBool) ⟩
+  (∀ (k : Clock) -> Σ[ b ∈ Bool ] bool2ty (A k) (B k) b )
+    Iso⟨ Iso-∀clock-Σ bool-clock-irrel ⟩
+  (Σ[ b ∈ Bool ] ∀ k -> bool2ty (A k) (B k) b)
+    Iso⟨ Σ-cong-iso-snd (λ b → Eq-Iso (bool2ty-eq b)) ⟩
+    --  (cong (Iso ((x : Clock) → bool2ty (A x) (B x) b)) (bool2ty-eq b))
+  (Σ[ b ∈ Bool ] bool2ty (∀ k -> A k) (∀ k -> B k) b)
+    Iso⟨ invIso Iso-⊎-ΣBool ⟩
+  (∀ k -> A k) ⊎ (∀ k -> B k) ∎Iso
+
+-- Action of the above isomorphism
+Iso-Π-⊎-clk-fun : {A B : Clock -> Type} -> {f : (k : Clock) -> (A k ⊎ B k) } ->
+  Iso.fun Iso-Π-⊎-clk f ≡ {!!}
+Iso-Π-⊎-clk-fun {A} {B} {f} = {!!}
+
+
+
+L℧-iso : {k : Clock} -> {X : Type} -> Iso (L℧ k X) ((X ⊎ ⊤) ⊎ (▹_,_ k (L℧ k X)))
+L℧-iso {k} {X} = iso f g sec retr
+  where
+    f : L℧ k X → (X ⊎ ⊤) ⊎ (▹ k , L℧ k X)
+    f (η x) = inl (inl x)
+    f ℧ = inl (inr tt)
+    f (θ lx~) = inr lx~
+
+    g : (X ⊎ ⊤) ⊎ (▹ k , L℧ k X) -> L℧ k X
+    g (inl (inl x)) = η x
+    g (inl (inr tt)) = ℧
+    g (inr lx~) = θ lx~
+
+    sec : section f g
+    sec (inl (inl x)) = refl
+    sec (inl (inr tt)) = refl
+    sec (inr lx~) = refl
+
+    retr : retract f g
+    retr (η x) = refl
+    retr ℧ = refl
+    retr (θ x) = refl
+
+
+
+
+L℧F-iso : {X : Type} -> Iso (L℧F X) (((□ X) ⊎ ⊤) ⊎ (L℧F X))
+L℧F-iso {X} =
+  (∀ k -> L℧ k X)
+
+          Iso⟨ codomainIsoDep (λ k -> L℧-iso) ⟩
+  
+  (∀ k -> (X ⊎ ⊤) ⊎ (▹_,_ k (L℧ k X)))
+
+          Iso⟨ Iso-Π-⊎-clk ⟩
+
+  (∀ (k : Clock) -> (X ⊎ ⊤)) ⊎ (∀ k -> ▹_,_ k (L℧ k X))
+ 
+          Iso⟨ ⊎Iso Iso-Π-⊎-clk idIso ⟩
+  
+  ((∀ (k : Clock) -> X) ⊎ (∀ (k : Clock) -> ⊤)) ⊎
+       (∀ k -> ▹_,_ k (L℧ k X))
+       
+          Iso⟨ ⊎Iso
+                (⊎Iso idIso (Iso-∀kA-A Unit-clock-irrel))
+                force-iso ⟩
+                    
+  ((□ X) ⊎ ⊤) ⊎ (L℧F X) ∎Iso
+
+-- Characterizing the behavior of the isomorphism on specific inputs.
+rule-tru : {k k' : Clock} -> {i : I} ->
+  bool-clock-irrel (λ x → true) k k' i ≣ true
+rule-tru = {!!}
+
+rule-fls : {k k' : Clock} -> {i : I} ->
+  bool-clock-irrel (λ x → false) k k' i ≣ false
+rule-fls = {!!}
+
+{-# REWRITE rule-tru rule-fls #-}
+
+
+
+
+
+lem-iso : {A B : Type} -> (iAB : Iso A B) -> (a : A) -> (b : B) ->
+  Iso.fun iAB a ≡ b -> Iso.inv iAB b ≡ a
+lem-iso iAB a b H =
+  Iso.inv iAB b                ≡⟨ sym (λ i -> Iso.inv iAB (H i) ) ⟩
+  Iso.inv iAB (Iso.fun iAB a)  ≡⟨ Iso.leftInv iAB a ⟩
+  a ∎
+
+L℧F-iso-η : {X : Type} -> (x : □ X) ->
+  Iso.fun L℧F-iso (ηF x) ≡ (inl (inl x))
+L℧F-iso-η x = cong inl (cong inl (clock-ext (λ k -> {!!})))
+
+L℧F-iso-℧ : {X : Type} ->
+  Iso.fun (L℧F-iso {X}) ℧F ≡ inl (inr tt)
+L℧F-iso-℧ = cong inl refl
+
+L℧F-iso-θ : {X : Type} -> (l : L℧F X) ->
+  Iso.fun (L℧F-iso {X}) (λ k -> θ (next (l k))) ≡ inr l
+L℧F-iso-θ l = cong inr (clock-ext (λ k -> {!!}))
+
+L℧F-iso-η-inv : {X : Type} ->
+  (l : L℧F X) -> (x : □ X) -> Iso.fun L℧F-iso l ≡ (inl (inl x)) ->
+  l ≡ (ηF x)
+L℧F-iso-η-inv l x H = isoFunInjective L℧F-iso l (ηF x)
+  (Iso.fun L℧F-iso l ≡⟨ H  ⟩
+  inl (inl x)        ≡⟨ sym (L℧F-iso-η x) ⟩
+  Iso.fun L℧F-iso (ηF x) ∎)
+
+
+
+
+-- In the special case where X is clock-irrelevant, we can simplify the
+-- above isomorphism further by replacing □ X with X.
+L℧F-iso-irrel : {X : Type} -> clock-irrel X -> Iso (L℧F X) ((X ⊎ ⊤) ⊎ (L℧F X))
+L℧F-iso-irrel {X} H-irrel =
+  L℧F X                     Iso⟨ L℧F-iso ⟩
+  ((□ X) ⊎ ⊤) ⊎ (L℧F X)     Iso⟨ ⊎Iso (⊎Iso (Iso-∀kA-A H-irrel) idIso) idIso ⟩
+  (X ⊎ ⊤) ⊎ (L℧F X) ∎Iso
+
+
+unfold-L℧F : {X : Type} -> clock-irrel X -> (L℧F X) ≡ ((X ⊎ ⊤) ⊎ (L℧F X))
+unfold-L℧F H = ua (isoToEquiv (L℧F-iso-irrel H))