coe of V #90
coe of V #90
Conversation
|
@favonia Good catch! Can you explain what you mean by your question though? |
|
What is the best way to have multiple implementations of Kan operations in redtt? |
|
@favonia Ahh, I see... Right now we don't have any infrastructure for propagating settings or flags through the program state. I guess you could just set a flag as a reference somewhere, not sure what's best. |
|
Anyways, I want to implement both @mortberg's new version and what's in my private note. |
|
Ultimately I dream of a user-exposed flag for |
favonia
force-pushed
the
coe-of-V
branch
4 times, most recently
from
dc48beb to
4ca1f55
Compare
src/lib/Val.ml
Outdated
| make_hcom (Star.make D.dim1 (D.named y)) ty cap msys | ||
| in | ||
| let el0, face_front = | ||
| let mode = `SPLIT_COERCION in (* how should we switch this? *) |
src/lib/Val.ml
Outdated
| match mode with | ||
| | `SPLIT_COERCION -> | ||
| begin | ||
| match D.unleash r (* favonia: is this really okay?! *) with |
There was a problem hiding this comment.
@jonsterling Is this really okay?
There was a problem hiding this comment.
I'm a tiny it worried about it, but let me double check it; it kind of depends on how unleash is implemented whether this makes any sense.
There was a problem hiding this comment.
@favonia This code is probably not going to do the right thing; instead, I think you should pattern match on the result of DimGeneric.make r, and in the Ok case, use the DimGeneric.atom operation that I have just now added.
|
@mortberg Perhaps you can clearly see why I still did not give up the split-then-coercion version. The only differences are in |
src/lib/Val.ml
Outdated
| el0, face_front | ||
| end | ||
| | `UNIFORM_HCOM -> | ||
| (* favonia: because there is no (easy) way to generate Sg in the semanitc domain, |
There was a problem hiding this comment.
I can show you a trick I learned from @mortberg to do this 😉
There was a problem hiding this comment.
Haha, I'm not sure exactly what you are referring to... But I bet it's a brilliant idea :)
There was a problem hiding this comment.
The trick is to write the term in the term language / syntax with some free variables, and then evaluate it in an environment that has the things you want to dump into there. I think there is an example of doing this somewhere in the code (I did this for equivalences)
There was a problem hiding this comment.
Ah right! That is neat indeed :)
There was a problem hiding this comment.
Oh I thought we do not have to bow to the darkness... @jonsterling Is there a helper function to create a good old variable from a string? I am worried about messing up with spine/cmd/head.
src/lib/Val.ml
Outdated
| match mode with | ||
| | `SPLIT_COERCION -> | ||
| begin | ||
| match D.unleash r (* favonia: is this really okay?! *) with |
There was a problem hiding this comment.
@favonia This code is probably not going to do the right thing; instead, I think you should pattern match on the result of DimGeneric.make r, and in the Ok case, use the DimGeneric.atom operation that I have just now added.
src/lib/Val.ml
Outdated
| in | ||
| (el0 D.dim1, face_front) | ||
| | `UNICORN -> | ||
| failwith "too immortal; not suitable for mortal beings" |
| let fiber0_ty b = | ||
| let var i = Tm.up @@ Tm.var i `Only in | ||
| eval (R.emp ()) [Val ty00; Val ty10; Val (car equiv0); Val b] @@ | ||
| Tm.Macro.fiber (var 0) (var 1) (var 2) (var 3) |
|
@jonsterling Thanks, but I think your trust is misplaced---I only trust myself in creating bugs. 🤣 (Wait, what if the bug I created has a bug in itself that makes it a non-bug?) |
|
@favonia It's like Dr McCoy explained to Spock in "Star Trek IV: The Voyage Home"
|
Fix #42. The current code is actually incorrect---the 0/1 cases only make sense when
x=yinx.V_y(...).What is the immortal way to have alternative dynamics? @jonsterling