From 4ffb0d3c07150e4078ec7409929f9b76efe37d65 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 20 Oct 2022 12:05:44 -0400
Subject: [PATCH] A simpler definition of Dyn?
---
formalizations/guarded-cubical/ErrorDomains.agda | 7 +++++--
formalizations/guarded-cubical/Later.agda | 4 ++--
2 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/formalizations/guarded-cubical/ErrorDomains.agda b/formalizations/guarded-cubical/ErrorDomains.agda
index 9377ebc..c6a98b7 100644
--- a/formalizations/guarded-cubical/ErrorDomains.agda
+++ b/formalizations/guarded-cubical/ErrorDomains.agda
@@ -348,17 +348,20 @@ data Dyn' (D : ▹ Type) : Type where
nat : ℕ -> Dyn' D
arr : ▸ (λ t → D t -> L℧ (D t)) -> Dyn' D
+-- Would this Dyn be better?
+data Dyn'' (D : ▹ Type) : Type where
+ nat : ℕ -> Dyn'' D
+ arr : (▸ D -> L℧ (Dyn'' D)) -> Dyn'' D
+
Dyn : Type
Dyn = fix Dyn'
-
-- Embedding-projection pairs
record EP (A B : Set) : Set where
field
emb : A -> B
proj : B -> L℧ A
-
-- E-P Pair for a type with itself
EP-id : (A : Type) -> EP A A
EP-id A = record {
diff --git a/formalizations/guarded-cubical/Later.agda b/formalizations/guarded-cubical/Later.agda
index dba75af..9e2368c 100644
--- a/formalizations/guarded-cubical/Later.agda
+++ b/formalizations/guarded-cubical/Later.agda
@@ -31,10 +31,10 @@ private
k : Clock
▹_,_ : Clock → Set l → Set l
-▹ k , A = (@tick x : Tick k) → A
+▹ k , A = (@tick t : Tick k) → A
▸_ : ▹ k , Set l → Set l
-▸ A = (@tick x : Tick _) → A x
+▸ A = (@tick t : Tick _) → A t
next : A → ▹ k , A
next x _ = x
--
GitLab