New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Simplify CartesianKanOps/FunExtEquiv using "interpolation" on I #1001
Conversation
Your |
I just had a look, this seems very useful! It's not too hard to show that Regarding the name: Why not call it |
Indeed, calling it |
So, interpolate in Cubical.Foundations.Interpolate, then? I can update the MR. (Or "interp"? It seems to occur in various computer math libraries...) It could just go in CartesianKanOps, even private. Or maybe it doesn't even need a name, like @kangrongji said. It is easy to define yourself or even (in simple cases) use directly when you want it. I created Erp.agda:
About the name, I just like short names, and I like to do nested erps. Here is one example I have handy. Compare: rot90 : (p : Ω² A x) → p ≡ (λ i j → p j (~ i))
rot90 p t i j =
hcomp (λ l → λ { (t = i0) → p (erp t i j) (erp t j (~ i))
; (t = i1) → p (erp t i j) (erp t j (~ i))
; (i = i0) → p (erp l (erp t i j) i0) (erp t j (~ i))
; (i = i1) → p (erp l (erp t i j) i1) (erp t j (~ i))
; (j = i0) → p (erp l (erp t i j) i0) (erp t j (~ i))
; (j = i1) → p (erp l (erp t i j) i1) (erp t j (~ i))
})
(p (erp t i j) (erp t j (~ i))) rot90 : (p : Ω² A x) → p ≡ (λ i j → p j (~ i))
rot90 p t i j =
hcomp (λ l → λ { (t = i0) → p (interpolate t i j) (interpolate t j (~ i))
; (t = i1) → p (interpolate t i j) (interpolate t j (~ i))
; (i = i0) → p (interpolate l (interpolate t i j) i0) (interpolate t j (~ i))
; (i = i1) → p (interpolate l (interpolate t i j) i1) (interpolate t j (~ i))
; (j = i0) → p (interpolate l (interpolate t i j) i0) (interpolate t j (~ i))
; (j = i1) → p (interpolate l (interpolate t i j) i1) (interpolate t j (~ i))
})
(p (interpolate t i j) (interpolate t j (~ i))) 🤷 I am happy to rename it in my personal files. I also like to excessively use By the way, @kangrongji, if you know about any other interesting "not so trivial" maps, e.g. in higher dimension, I would love to hear about them. 😄 |
I think it very valuable to have these things written down somewhere, and this library seems like a good place. Consider that cubical type theory is a niche thing that is (for me at least) hard to learn, so any resource that helps understand it better is appreciated. Even (or in particular) if it concerns "trivialities". Personally, I also find the ad-hoc interval expressions hard to read; there's not enough context to see at a glance what their intent is. I think having descriptive names, such as
Agree, short names are nice when it's unambiguous what they mean. Agda supports import Cubical.Foundations.Interpolate renaming (interpolate to erp) public is something I'd put in my personal prelude. For library use, I'd keep a more descriptive name though and use an alias whenever it becomes bothersome.
I haven't quite figured it out yet, but are there 3D-analouges of |
Yes! I wondered if @kangrongji might be a Cylon. 😉
I have De Morgan and Kleene search procedures that sometimes work. If you can tell me the requirements you seek (as if |
Looks good to me. |
That's cool. What about using |
Btw, a bit trivial but worth to mention, this operation can interpolate between any |
This might be a reasonable compromise? What I don't like about |
Another suggestion: I think |
I just remembered this PR... It looks like last time, we were all busy bike-shedding names for |
Sorry! I have renamed the operator to |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me!
Oops, CI unhappy... Please fix |
@mortberg so sorry 🤦 should be better now ( |
Attempted to fix the new CI problem, sorry again. I am trying to run |
I've checked baf40df locally. Everything still type checks fine. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think this should go in the Core. The idea of the Core is to expose builtins nicer, but the rest of the library should rely on what is in the Prelude.
f1deb7d
to
7bb3d99
Compare
Sorry... I shouldn't have tried to change things. I reverted to the previous approved state, and changed only the name "erp" to "interpolateI". I hope that's OK. 😄 Unfortunately I am unable right now to run CI checks locally, I hope they will pass...
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good to me, merging if CI is happy
Attempted CI fix. I am praying that this PR can finally be over... I still haven't been able to run checks locally but I could try again soon. |
Now there is a conflict... Can you rebase on current master? We changed it so that Foundations.Everything is automatically generated, so no need to edit it manually anymore |
Nice! Rebased. 🙏 🙏 |
The CI was finally happy so I merged. Thanks for the contribution! |
[note: in the latest, the
erp
operator has been renamed tointerpolateI
and is defined inCubical.Core.Interpolate
]Here I added an "interpolation" operator on the interval, in Cubical.Foundations.Erp:
I have found the
erp
operator to be very useful generally, so I think it is worth exposing in the library.Using
erp
, I simplified CartesianKanOps and FunExtEquiv.I am not really sure whether the changes to CartesianKanOps and FunExtEquiv are worth doing. The new versions seem simpler, but I don't have any real examples where they improve performance or make proofs easier, and I guess this might break some user code.
I have also added
funExtNonDep
for paths in non-dependent function types (but where both domain and codomain depend on the interval) which can be even simpler than the newfunExtDep
. Maybe there is a better name thanfunExtNonDep
?