Show in Agda that Machine has a predomain structure
We defined the Machine
type as the coninductive type of computations that at each step can either return a value or continue running.
In order to even state the isomorphism of predomains satisfied by the "global" Dyn predomain (see #3), we need to show in Agda that Machine
has a predomain structure. This will involve:
-
Showing that Machine
is a Set. This will also require to show thatState
(the inductive type of machine states defined mutually withMachine
s) is a Set. This will require adding a squash constructor to theState
type and then adding pattern matching cases for all of the functions defined onState
to accomodate this new constructor. -
Choose the appropriate ordering on Machines to be used for the predomain structure. Are we using a step-insensitive or step-sensitive ordering? -
Prove that ordering is prop-valued, reflexive, transitive, and antisymmetric.