jonsterling
Add --without-K everywhere
However, we now have: https://github.com/jonsterling/cost-refinement-lab/blob/ffad8eafec348a9a890723e35faf9d02ff0a8db4/src/Calf/Types/Eq.agda#L17-L18
Although, it's only used here: https://github.com/jonsterling/cost-refinement-lab/blob/ffad8eafec348a9a890723e35faf9d02ff0a8db4/src/Calf/Noninterference.agda#L22
(Perhaps Noninterference should be with K, and eq/uni should be defined using uip rather than postulated? Not sure.)
i feel it should be possible to prove that theorem without uip, but i’ll have to look into it.
Sent from my iPhone
On Jul 7, 2021, at 2:59 AM, Harrison Grodin @.***> wrote:
However, we now have: https://github.com/jonsterling/cost-refinement-lab/blob/ffad8eafec348a9a890723e35faf9d02ff0a8db4/src/Calf/Types/Eq.agda#L17-L18
Although, it's only used here: https://github.com/jonsterling/cost-refinement-lab/blob/ffad8eafec348a9a890723e35faf9d02ff0a8db4/src/Calf/Noninterference.agda#L22
(Perhaps Noninterference should be with K, and eq/uni should be defined using uip rather than postulated? Not sure.)
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.
I think the way the eq type is being used currently suggests that it should be a negative type whose computations are the Agda equality between the relevant terms. Eq would have the trivial algebra structure, which would justify the interpretation as meta-level equality when K is assumed.
Do we want to put these in before submission, or leave as-is (some files with, some without)?