Prove in Agda that the "global" Dyn predomain satisfies an isomorphism
For a fixed clock k, we defined the Dyn predomain such that
Dyn k ≅ Nat + ▹k(Dyn k -->mon (L k (Dyn k)))
(But currently, we only proved in Agda that the underlying types are isomorphic, not the predomains themselves! See checklist below.)
Now consider the "global" version of this predomain, denoted GDyn
, with underlying type given by
∀ k . Dyn k
and relation defined by
x ≤ y iff ∀ k. (x k) ≤ (y k) in (Dyn k)
@ericgio sketched a proof on paper that GDyn
satisfies a global version of the above isomorphism, i.e.,
GDyn ≅ (Nat + (GDyn -->mon (Machine GDyn)))
The proof involves showing that we can distribute the clock quantifier over the function arrow; this makes use of a property of Dyn, which in turn follows from a property of all Error Domains.
The goal of this Issue is to formalize all of this in the Agda development. We want to show that this isomorphism holds at the level of predomains and not just at the level of the underlying types. This will involve showing that the function underlying the isomorphism is monotone, which in turn will require working with the relations of both sides.
-
Show for a fixed clock k, that Dyn k ≅ Nat + ▹k(Dyn k -->mon (L k (Dyn k)))
holds as an isomorphism of predomains -
Define GDyn, the "global" version of the Dyn predomain -
Show that GDyn ≅ (Nat + (GDyn -->mon (Machine GDyn)))
holds at the level of types-
Show that we can distribute the clock quantifier over the function arrow, i.e., ∀ k . (Dyn k -->mon (L k (Dyn k))) ≅ ((∀ k . Dyn k) -->mon (∀ k . L k (Dyn k)))
-
Show that (∀ k . L k (Dyn k)) is isomorphic to Machine GDyn
-
-
Show that the above isomorphism holds at the level of predomains