search

jonsterling / agda-calf

A cost-aware logical framework, embedded in Agda.
https://jonsterling.github.io/agda-calf/
Apache License 2.0
55 stars 2 forks source link

Add --without-K everywhere #27

Closed HarrisonGrodin closed 1 year ago

HarrisonGrodin commented 3 years ago

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.)

jonsterling commented 3 years ago

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.

kaonn commented 3 years ago

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.

HarrisonGrodin commented 3 years ago

Do we want to put these in before submission, or leave as-is (some files with, some without)?

kaonn commented 3 years ago

No really sure what this pr does, but let's just leave it for now.