Guarded Cubical with clocks

Primitives.agda

module Prims where
  primitive
    primLockUniv : Set₁

open Prims renaming (primLockUniv to LockU) public

postulate
  Cl : Set
  k0 : Cl
  Tick : Cl → LockU

▹ : ∀ {l} → Cl → Set l → Set l
▹ k A = (@tick x : Tick k) -> A

▸ : ∀ {l} k → ▹ k (Set l) → Set l
▸ k A = (@tick x : Tick k) → A x

postulate
  tick-irr : ∀ {A : Set}{k : Cl} (x : ▹ k A) → ▸ k \ α → ▸ k \ β → x α ≡ x β

postulate
  dfix : ∀ {k} {l} {A : Set l} → (▹ k A → A) → ▹ k A
  pfix : ∀ {k} {l} {A : Set l} (f : ▹ k A → A) → dfix f ≡ (\ _ → f (dfix f))

  force : ∀ {l} {A : Cl → Set l} → (∀ k → ▹ k (A k)) → ∀ k → A k
  force-delay : ∀ {l} {A : Cl → Set l} → (f : ∀ k → ▹ k (A k)) → ∀ k → ▸ k \ α → force f k ≡ f k α
  delay-force : ∀ {l} {A : Cl → Set l} → (f : ∀ k → A k)       → ∀ k → force (\ k α → f k) k ≡ f k
  force^ : ∀ {l} {A : ∀ k → ▹ k (Set l)} → (∀ k → ▸ k (A k)) → ∀ k → force A k
-- No more postulates after this line.

private
  variable
    l : Level
    A B : Set l
    k : Cl

next : A → ▹ k A
next x _ = x

_⊛_ : ▹ k (A → B) → ▹ k A → ▹ k B
_⊛_ f x a = f a (x a)

map▹ : (f : A → B) → ▹ k A → ▹ k B
map▹ f x α = f (x α)

later-ext : ∀ {l} {A : Set l} → {f g : ▹ k A} → (▸ k \ α → f α ≡ g α) → f ≡ g
later-ext eq = \ i α → eq α i

pfix' : ∀ {l} {A : Set l} (f : ▹ k A → A) → ▸ k \ α → dfix f α ≡ f (dfix f)
pfix' f α i = pfix f i α

fix : ∀ {l} {A : Set l} → (▹ k A → A) → A
fix f = f (dfix f)

fix-eq : ∀ {l} {A : Set l} → (f : ▹ k A → A) → fix f ≡ f (\ _ → fix f)
fix-eq f = \ i →  f (pfix f i)

delay : ∀ {A : Cl → Set} → (∀ k → A k) → ∀ k → ▹ k (A k)
delay a k _ = a k

Later-Alg[_]_ : ∀ {l} → Cl → Set l → Set l
Later-Alg[ k ] A = ▹ k A → A

What's missing is equalities for "force" (or directly the diamond tick) and ways to commute clock quantification and HITs.

…

On Wed, Feb 24, 2021 at 5:43 PM Liang-Ting Chen ***@***.***> wrote: ***@***.**** commented on this gist. ------------------------------ Is the only thing missing the judgemental equality in Clocked Cubical Type Theory? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <https://gist.github.com/ee9c0a7fe61db3aa0036715800edcd1d#gistcomment-3643956>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAA76THV23WP54SOPAEQIGTTAUUCPANCNFSM4YE3BKJQ> .

Alright, that sounds useful enough to me already. By the way, is it reasonable to postulate the diamond tick and use the REWRITE pragma to introduce necessary rewrite rules for those missing judgemental equalities?

Forgot to say: thank you so much!

The typing rule for diamond tick seems hard to reproduce as a postulate, though maybe you could make it private and use it as the implementation of force?

But the current implementation only accepts lock variables,

lock should be a var
when inferring the type of t ◇

so the following postulate

module _ where
  private
    postulate
      ◇ : {k : Cl} → Tick k

is not helpful to express the judgemental equalities about the diamond tick.

Maybe I will just wait for it to be implemented. :-)