From 19fb32ba10e7288ed35bf8484e34d9855b39b44d Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 21 Jul 2022 11:13:58 -0400
Subject: [PATCH] axiomatize some clocks?

---
 formalizations/guarded-cubical/Later.agda | 58 +++++++++++++----------
 1 file changed, 32 insertions(+), 26 deletions(-)

diff --git a/formalizations/guarded-cubical/Later.agda b/formalizations/guarded-cubical/Later.agda
index 3d5f648..f41e863 100644
--- a/formalizations/guarded-cubical/Later.agda
+++ b/formalizations/guarded-cubical/Later.agda
@@ -1,10 +1,10 @@
 {-# OPTIONS --cubical --rewriting --guarded #-}
 module Later where
 
--- | This file is from the supplementary material for the paper
--- | https://doi.org/10.1145/3372885.3373814
--- | and is originally written by NiccolÃ² Veltri and Andrea Vezzosi
--- | see the LICENSE.txt for their license.
+-- | This file is adapted from the supplementary material for the
+-- | paper https://doi.org/10.1145/3372885.3373814, originally written
+-- | by NiccolÃ² Veltri and Andrea Vezzosi see the LICENSE.txt for
+-- | their license.
 
 open import Agda.Builtin.Equality renaming (_â‰¡_ to _â‰£_)
 open import Agda.Builtin.Equality.Rewrite
@@ -19,56 +19,62 @@ module Prims where
 
 open Prims renaming (primLockUniv to LockU) public
 
+-- We postulate Tick as it is supposed to be an abstract sort.
+postulate
+  Clock : Set
+  Tick : Clock â†’ LockU
+
 private
   variable
     l : Level
     A B : Set l
+    k : Clock
 
--- We postulate Tick as it is supposed to be an abstract sort.
-postulate
-  Tick : LockU
-
-â–¹_ : âˆ€ {l} â†’ Set l â†’ Set l
-â–¹_ A = (@tick x : Tick) -> A
+â–¹_,_ : Clock â†’ Set l â†’ Set l
+â–¹ k , A = (@tick x : Tick k) â†’ A
 
-â–¸_ : âˆ€ {l} â†’ â–¹ Set l â†’ Set l
-â–¸ A = (@tick x : Tick) â†’ A x
+â–¸_ : â–¹ k , Set l â†’ Set l
+â–¸ A = (@tick x : Tick _) â†’ A x
 
-next : A â†’ â–¹ A
+next : A â†’ â–¹ k , A
 next x _ = x
 
-_âŠ›_ : â–¹ (A â†’ B) â†’ â–¹ A â†’ â–¹ B
+_âŠ›_ : â–¹ k , (A â†’ B) â†’ â–¹ k , A â†’ â–¹ k , B
 _âŠ›_ f x a = f a (x a)
 
-mapâ–¹ : (f : A â†’ B) â†’ â–¹ A â†’ â–¹ B
+mapâ–¹ : (f : A â†’ B) â†’ â–¹ k , A â†’ â–¹ k , B
 mapâ–¹ f x Î± = f (x Î±)
 
 -- The behaviour of fix is encoded with rewrite rules, following the
--- definitional equalities of TCTT.
+-- definitional equalities of Clocked CTT.
 postulate
-  dfix : âˆ€ {l} {A : Set l} â†’ (f : â–¹ A â†’ A) â†’ I â†’ â–¹ A
-  dfix-beta : âˆ€ {l} {A : Set l} â†’ (f : â–¹ A â†’ A) â†’ dfix f i1 â‰£ next (f (dfix f i0))
+  dfix : âˆ€ {k}{l} {A : Set l} â†’ (f : â–¹ k , A â†’ A) â†’ I â†’ â–¹ k , A
+  dfix-beta : âˆ€ {l} {A : Set l} â†’ (f : â–¹ k , A â†’ A) â†’ dfix f i1 â‰£ next (f (dfix f i0))
 
 {-# REWRITE dfix-beta #-}
 
-pfix : âˆ€ {l} {A : Set l} â†’ (f : â–¹ A â†’ A) â†’ dfix f i0 â‰¡ next (f (dfix f i0))
+pfix : âˆ€ {l} {A : Set l} â†’ (f : â–¹ k , A â†’ A) â†’ dfix f i0 â‰¡ next (f (dfix f i0))
 pfix f i = dfix f i
 
 abstract
-  fix : âˆ€ {l} {A : Set l} â†’ (f : â–¹ A â†’ A) â†’ A
+  fix : âˆ€ {l} {A : Set l} â†’ (f : â–¹ k , A â†’ A) â†’ A
   fix f = f (pfix f i0)
 
-  fix-eq : âˆ€ {l} {A : Set l} â†’ (f : â–¹ A â†’ A) â†’ fix f â‰¡ f (next (fix f))
+  fix-eq : âˆ€ {l} {A : Set l} â†’ (f : â–¹ k , A â†’ A) â†’ fix f â‰¡ f (next (fix f))
   fix-eq f = cong f (pfix f)
 
-later-ext : âˆ€ {A : â–¹ Set} â†’ {f g : â–¸ A} â†’ (â–¸ \ a â†’ f a â‰¡ g a) â†’ f â‰¡ g
+later-ext : âˆ€ {A : â–¹ k , Set} â†’ {f g : â–¸ A} â†’ (â–¸ \ a â†’ f a â‰¡ g a) â†’ f â‰¡ g
 later-ext eq i a = eq a i
 
+transpLater : âˆ€ (A : I â†’ â–¹ k , Set) â†’ â–¸ (A i0) â†’ â–¸ (A i1)
+transpLater A u0 a = transp (\ i â†’ A i a) i0 (u0 a)
 
+hcompLater : âˆ€ (A : â–¹ k , Set) Ï† (u : I â†’ Partial Ï† (â–¸ A)) â†’ (u0 : â–¸ A [ Ï† â†¦ u i0 ]) â†’ â–¸ A
+hcompLater A Ï† u u0 a = hcomp (\ { i (Ï† = i1) â†’ u i 1=1 a }) (outS u0 a)
 
+postulate
+  force : (âˆ€ k â†’ (â–¹ k , A)) â†’ (âˆ€ (k : Clock) â†’ A)
 
-transpLater : âˆ€ (A : I â†’ â–¹ Set) â†’ â–¸ (A i0) â†’ â–¸ (A i1)
-transpLater A u0 a = transp (\ i â†’ A i a) i0 (u0 a)
+postulate
+  force-beta : âˆ€ {A : Set l} (x : A) â†’ force (Î» k _ â†’ x) â‰£ Î» k â†’ x
 
-hcompLater : âˆ€ (A : â–¹ Set) Ï† (u : I â†’ Partial Ï† (â–¸ A)) â†’ (u0 : â–¸ A [ Ï† â†¦ u i0 ]) â†’ â–¸ A
-hcompLater A Ï† u u0 a = hcomp (\ { i (Ï† = i1) â†’ u i 1=1 a }) (outS u0 a)
-- 
GitLab