From 5d1df60888ab9716c2ac98ac877ad6f200be5202 Mon Sep 17 00:00:00 2001
From: Eric Giovannini <ecg19@seas.upenn.edu>
Date: Tue, 3 Oct 2023 11:50:43 -0400
Subject: [PATCH] Inductive definition of perturbations

---
 .../guarded-cubical/Syntax/Perturbation.agda  | 103 ++++++++++++++++++
 1 file changed, 103 insertions(+)
 create mode 100644 formalizations/guarded-cubical/Syntax/Perturbation.agda

diff --git a/formalizations/guarded-cubical/Syntax/Perturbation.agda b/formalizations/guarded-cubical/Syntax/Perturbation.agda
new file mode 100644
index 0000000..3d978ab
--- /dev/null
+++ b/formalizations/guarded-cubical/Syntax/Perturbation.agda
@@ -0,0 +1,103 @@
+module Syntax.Perturbation where
+
+
+-- The intensional syntax, which is quotiented by Î²Î· equivalence and
+-- order equivalence but where casts take observable steps.
+
+open import Cubical.Foundations.Prelude renaming (comp to compose)
+
+
+open import Syntax.Types
+
+open TyPrec
+open CtxPrec
+
+private
+ variable
+   Î” Î“ Î˜ Z Î”' Î“' Î˜' Z' : Ctx
+   R S T U R' S' T' U' : Ty
+   B B' C C' D D' : Î“ âŠ‘ctx Î“'
+   b b' c c' d d' : S âŠ‘ S'
+
+data Pertá´± : Ty -> Type
+data Pertá´¾ : Ty -> Type
+
+data Pertá´± where
+  id : Pertá´± S
+  _â‡€_ : âˆ€ {S T} -> Pertá´¾ S -> Pertá´± T -> Pertá´± (S â‡€ T)
+  PertD : Pertá´± nat -> Pertá´± (dyn â‡€ dyn) -> Pertá´± dyn
+
+data Pertá´¾ where
+  Î´Pert : Pertá´¾ S -> Pertá´¾ S
+  id : Pertá´¾ S
+  _â‡€_ : âˆ€ {S T} -> Pertá´± S -> Pertá´¾ T -> Pertá´¾ (S â‡€ T)
+  PertD : Pertá´¾ nat -> Pertá´¾ (dyn â‡€ dyn) -> Pertá´¾ dyn
+
+-- Pushing and pulling perturbations across type precision
+
+PushP : (c : S âŠ‘ T) -> Pertá´¾ S -> Pertá´¾ T
+PushE : (c : S âŠ‘ T) -> Pertá´± S -> Pertá´± T
+
+PushP c (Î´Pert p) = Î´Pert (PushP c p)
+PushP c id = id
+PushP (ci â‡€ co) (Î´i â‡€ Î´o) = PushE ci Î´i â‡€ PushP co Î´o
+PushP (inj-arr c) (Î´i â‡€ Î´o) = PertD id (PushP c (Î´i â‡€ Î´o))
+PushP dyn (PertD Î´n Î´f) = PertD Î´n Î´f
+
+PushE c id = id
+PushE (ci â‡€ co) (Î´i â‡€ Î´o) = PushP ci Î´i â‡€ PushE co Î´o
+PushE (inj-arr c) (Î´i â‡€ Î´o) = PertD id (PushE c (Î´i â‡€ Î´o))
+PushE dyn (PertD Î´n Î´f) = PertD Î´n Î´f
+
+
+PullE : (c : S âŠ‘ T) -> Pertá´± T -> Pertá´± S
+PullP : (c : S âŠ‘ T) -> Pertá´¾ T -> Pertá´¾ S
+
+PullE c id = id
+PullE (ci â‡€ co) (Î´i â‡€ Î´o) = PullP ci Î´i â‡€ PullE co Î´o
+PullE dyn (PertD Î´n Î´f) = PertD Î´n Î´f
+PullE inj-nat (PertD Î´n Î´f) = Î´n
+PullE (inj-arr c) (PertD Î´n Î´f) = PullE c Î´f
+
+PullP c (Î´Pert p) = Î´Pert (PullP c p)
+PullP c id = id
+PullP (ci â‡€ co) (Î´i â‡€ Î´o) = PullE ci Î´i â‡€ PullP co Î´o
+PullP dyn (PertD Î´n Î´f) = PertD Î´n Î´f
+PullP inj-nat (PertD Î´n Î´f) = Î´n
+PullP (inj-arr c) (PertD Î´n Î´f) = PullP c Î´f
+
+
+
+-- Perturbations from type precision derivations
+
+-- Left (e and p)
+Î´l-e-pert : S âŠ‘ T -> Pertá´± S
+Î´l-p-pert : S âŠ‘ T -> Pertá´¾ S
+
+Î´l-e-pert nat = id
+Î´l-e-pert dyn = id
+Î´l-e-pert (ci â‡€ co) = (Î´l-p-pert ci) â‡€ (Î´l-e-pert co)
+Î´l-e-pert inj-nat = id
+Î´l-e-pert (inj-arr c) = Î´l-e-pert c
+
+Î´l-p-pert nat = id
+Î´l-p-pert dyn = id
+Î´l-p-pert (ci â‡€ co) = (Î´l-e-pert ci) â‡€ (Î´l-p-pert co)
+Î´l-p-pert inj-nat = id
+Î´l-p-pert (inj-arr c) = Î´Pert (Î´l-p-pert c)
+
+-- Right (e and p)
+Î´r-e-pert : S âŠ‘ T -> Pertá´± T
+Î´r-p-pert : S âŠ‘ T -> Pertá´¾ T
+
+Î´r-e-pert nat = id
+Î´r-e-pert dyn = id
+Î´r-e-pert (ci â‡€ co) = (Î´r-p-pert ci) â‡€ (Î´r-e-pert co)
+Î´r-e-pert inj-nat = id
+Î´r-e-pert (inj-arr c) = PertD id (Î´r-e-pert c) -- correct?
+
+Î´r-p-pert nat = id
+Î´r-p-pert dyn = id
+Î´r-p-pert (ci â‡€ co) = (Î´r-e-pert ci) â‡€ (Î´r-p-pert co)
+Î´r-p-pert inj-nat = id -- correct?
+Î´r-p-pert (inj-arr c) =  PertD id (Î´Pert (Î´r-p-pert c))  -- wrong: Î´Pert (PertD id (Î´r-p-pert c)) 
-- 
GitLab