From c08d42022bca55bd29be797ffea304f53acb5376 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 21 Jul 2022 12:03:52 -0400
Subject: [PATCH] Start the guarded cubical experiment
---
.../guarded-cubical/ErrorDomains.agda | 67 ++++++++++++++++++-
1 file changed, 66 insertions(+), 1 deletion(-)
diff --git a/formalizations/guarded-cubical/ErrorDomains.agda b/formalizations/guarded-cubical/ErrorDomains.agda
index a6b1255..7772fc3 100644
--- a/formalizations/guarded-cubical/ErrorDomains.agda
+++ b/formalizations/guarded-cubical/ErrorDomains.agda
@@ -2,4 +2,69 @@
open import Later
--- | TODO: everything lol
+module ErrorDomains(k : Clock) where
+
+open import Cubical.Relation.Binary
+open import Cubical.Relation.Binary.Poset
+
+open import Cubical.Data.Sigma
+
+private
+ variable
+ l : Level
+ A B : Set l
+private
+ ▹_ : Set l → Set l
+ ▹_ A = ▹_,_ k A
+
+Predomain : Set₁
+Predomain = Poset ℓ-zero ℓ-zero
+record MonFun (X Y : Predomain) : Set where
+ module X = PosetStr (X .snd)
+ module Y = PosetStr (Y .snd)
+ _≤X_ = X._≤_
+ _≤Y_ = Y._≤_
+ field
+ f : (X .fst) → (Y .fst)
+ isMon : ∀ {x y} → x ≤X y → f x ≤Y f y
+
+▸' : ▹ Predomain → Predomain
+▸' X = ((@tick x : Tick k) → (X x) .fst) ,
+ posetstr (fix {k = k} (λ _,_≤_ x₁ x₂ → ▸ λ x → x , x₁ ≤ x₂))
+ (fix {k = k} λ proofs → isposet {!!} {!!} {!!} {!!} {!!})
+
+▸''_ : Predomain → Predomain
+▸'' X = ▸' (next X)
+
+record ErrorDomain : Set₁ where
+ field
+ X : Predomain
+ module X = PosetStr (X .snd)
+ _≤_ = X._≤_
+ field
+ ℧ : X .fst
+ ℧⊥ : ∀ x → ℧ ≤ x
+
+ θ : MonFun (▸'' X) X
+
+data L℧₀ (X : Set) : Set where
+ η₀ : X → L℧₀ X
+ ℧ : L℧₀ X
+ θ₀ : ▹ (L℧₀ X) → L℧₀ X
+
+L℧ : Predomain → ErrorDomain
+L℧ X = record { X = L℧X ; ℧ = ℧ ; ℧⊥ = {!!} ; θ = record { f = θ₀ ; isMon = {!!} } }
+ where
+ L℧X : Predomain
+ L℧X = L℧₀ (X .fst) , {!!}
+
+-- | TODO:
+-- | 1. monotone monad structure
+-- | 2. strict functions
+-- | 3. UMP?
+-- | 4. show that later preserves domain structures
+-- | 5. Solve some example recursive domain equations
+-- | 6. Program in shallow embedded lambda calculus
+-- | 7. Embedding-Projection pairs!
+-- | 8. GLTC Syntax, Inequational theory
+-- | 9. Model of terms & inequational theory
--
GitLab