From 6e0ac743d51516c0a6aefc459d80e9445006248a Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 21 Mar 2023 14:51:16 -0400
Subject: [PATCH] Changes to Later.agda: add dependent force function (where
 the type can mention the clock); remove "global" clock-irrel axiom, instead
 axiomatize it on a per-type basis

---
 formalizations/guarded-cubical/Later.agda | 44 +++++++++++++++++++----
 1 file changed, 38 insertions(+), 6 deletions(-)

diff --git a/formalizations/guarded-cubical/Later.agda b/formalizations/guarded-cubical/Later.agda
index a074436..e68d77e 100644
--- a/formalizations/guarded-cubical/Later.agda
+++ b/formalizations/guarded-cubical/Later.agda
@@ -13,6 +13,8 @@ open import Agda.Builtin.Sigma
 open import Cubical.Core.Everything
 open import Cubical.Foundations.Everything
 
+open import Cubical.Data.Nat
+
 module Prims where
   primitive
     primLockUniv : Set₁
@@ -105,13 +107,14 @@ tr→tr' : {M : ▹ k , A} -> tick-irrelevance M -> tr' M
 
 -- The tick constant.
 postulate
-  _â—‡ : (k : Clock) -> Tick k
+  -- _â—‡ : (k : Clock) -> Tick k
+  â—‡ : {k : Clock} -> Tick k
 
 -- From Section V.C of Bahr et. al
 -- (See https://bahr.io/pubs/files/bahr17lics-paper.pdf).
 postulate
   tick-irrelevance-â—‡-refl : {A : Type} -> (M : â–¹ k , A) ->
-    (tick-irrelevance M (k ◇) (k ◇)) ≡ Cubical.Foundations.Everything.refl
+    (tick-irrelevance M (◇) (◇)) ≡ Cubical.Foundations.Everything.refl
       -- Should this use _≣_.refl instead?
 
 
@@ -127,6 +130,13 @@ next-Mt≡M' M t = next-Mt≡M M t
 
 
 
+-- "Dependent" forcing (where the type can mention the clock).
+-- This seems to be the correct type of the force function.
+
+postulate
+  force' : {A : Clock -> Type} -> (∀ k → (▹ k , A k)) → (∀ (k : Clock) → A k)
+
+
 
 
 -- Clock-related postulates.
@@ -136,12 +146,34 @@ postulate
 postulate
   k0 : Clock
 
+{-
 postulate
-  clock-irrel : {â„“ : Level} -> {A : Type â„“} ->
-    (M : ∀ (k : Clock) -> A) ->
-    (k k' : Clock) ->
-    M k ≡ M k'
+  nat-clock-irrel : (∀ (k : Clock) -> ℕ) ≡ ℕ
+-}
+
+-- Definition of clock irrelevance, parameterized by a specific type
+clock-irrel : Type -> Type
+clock-irrel A =
+  (M : ∀ (k : Clock) -> A) ->
+  (k k' : Clock) ->
+  M k ≡ M k'
+
+
+∀kA->A : (A : Type) ->
+  (∀ (k : Clock) -> A) -> A
+∀kA->A A f = f k0
+
+-- If A is clock irrelevant, then the above map is inverse
+-- to the map A -> ∀ k . A.
+
+
+postulate
+  nat-clock-irrel : clock-irrel â„•
+
 
+clock-ext : {ℓ : Level} {A : (k : Clock) -> Type ℓ} -> {M N : (k : Clock) -> A k} →
+  (∀ k → M k ≡ N k) → M ≡ N
+clock-ext eq i k = eq k i
 
 
 
-- 
GitLab