From 91440cb5b498c8673fc4cac19e2649410e7d00ac Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 30 May 2023 13:04:08 -0400
Subject: [PATCH] Move global lift code into separate file

---
 .../Results/IntensionalAdequacy.agda          | 220 +++--------
 .../guarded-cubical/Semantics/Global.agda     | 356 ++++++++++++++++++
 2 files changed, 409 insertions(+), 167 deletions(-)
 create mode 100644 formalizations/guarded-cubical/Semantics/Global.agda

diff --git a/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda b/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
index dcb58df..8cfe813 100644
--- a/formalizations/guarded-cubical/Results/IntensionalAdequacy.agda
+++ b/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 = {!!}
+    
+
diff --git a/formalizations/guarded-cubical/Semantics/Global.agda b/formalizations/guarded-cubical/Semantics/Global.agda
new file mode 100644
index 0000000..0b3b29f
--- /dev/null
+++ b/formalizations/guarded-cubical/Semantics/Global.agda
@@ -0,0 +1,356 @@
+{-# 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))
-- 
GitLab