axiomatize some clocks?

formalizations/guarded-cubical/Later.agda

 {-# 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)