Simplify CartesianKanOps/FunExtEquiv using "interpolation" on I

[pi3js2]

[note: in the latest, the erp operator has been renamed to interpolateI and is defined in Cubical.Core.Interpolate]

Here I added an "interpolation" operator on the interval, in Cubical.Foundations.Erp:

erp : I → I → I → I
erp t i j = (~ t ∧ i) ∨ (t ∧ j) ∨ (i ∧ j)

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 new funExtDep. Maybe there is a better name than funExtNonDep?

[kangrongji]

Your erp is the first "not so trivial" map between de Morgan cubes I³ → I, and I think it's the only one in this 3-dimensional case, up to certain renaming or involution. It's already used in many parts of the library to construct higher degenerate cubes as in here or here. I'm not sure if give it a name would make things more clear. Maybe it's a good idea. But the name erp looks a bit strange... It's just my personal view.

[phijor]

I just had a look, this seems very useful! It's not too hard to show that coei→j as defined in terms of erp is an equivalence (https://github.com/phijor/cubical/commit/cd210450eaa77142d7405ff5f007e9ba9482eb73). Since everything computes nicely, this turns into proofs of isEquiv (transport p) and transpEquiv : ∀ i → p i ≃ B (cf. https://github.com/agda/cubical/pull/1069) for free.

Regarding the name: Why not call it interp? This is in line with the pattern of primitive operations ending in p, like in transp and comp.

[mortberg]

Indeed, calling it interp or interpolate sounds good to me. Otherwise I think this could be merged? @ecavallo Any opinions?

[pi3js2]

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:

• to advertise to people who don't know about this thing, like me not very long ago...
• to provide a place to demonstrate the nice equations it satisfies. I have more equations to add, by the way.

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

:shrug: I am happy to rename it in my personal files.

I also like to excessively use erp (as you can see in the rot90 example.) But I have noticed that this is somewhat problematic; it seems that Agda tends not to normalize interval expressions very well, so using an erp when you don't need it can lead to unnecessarily complicated "normal" forms.

---

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. :smile:

[phijor]

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:

* to advertise to people who don't know about this thing, like me not very long ago...

* to provide a place to demonstrate the nice equations it satisfies. I have more equations to add, by the way.

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 squeeze, spread, coe and interpolate helps readability of low-level proofs a lot.

About the name, I just like short names, and I like to do nested erps. 🤷 I am happy to rename it in my personal files.

Agree, short names are nice when it's unambiguous what they mean. Agda supports renaming on import, so

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.

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 haven't quite figured it out yet, but are there 3D-analouges of erp and eqI? The equivalence I built in https://github.com/phijor/cubical/commit/cd210450eaa77142d7405ff5f007e9ba9482eb73 doesn't reduce to idIsEquiv on (i = i0 ∧ j = i0) or (i = i1 ∧ j = i1), but I think it could with slightly better interpolation.

[pi3js2]

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 squeeze, spread, coe and interpolate helps readability of low-level proofs a lot.

Yes! I wondered if @kangrongji might be a Cylon. :wink:

I haven't quite figured it out yet, but are there 3D-analouges of erp and eqI? The equivalence I built in phijor@cd21045 doesn't reduce to idIsEquiv on (i = i0 ∧ j = i0) or (i = i1 ∧ j = i1), but I think it could with slightly better interpolation.

I have De Morgan and Kleene search procedures that sometimes work. If you can tell me the requirements you seek (as if (i j k ... : I) -> Sub I ? ?) I can try running the search. Feel free to email me at <username>@proton.me if you like.

[ecavallo]

Indeed, calling it interp or interpolate sounds good to me. Otherwise I think this could be merged? @ecavallo Any opinions?

Looks good to me.

[kangrongji]

That's cool. What about using intp? not easy to pronounce though.

[kangrongji]

Btw, a bit trivial but worth to mention, this operation can interpolate between any u v : I^n -> I by writing (~ t ∧ u) ∨ (t ∧ v) ∨ (u ∧ v). More generally apply to each coordinates it can interpolate any maps I^m -> I^n.

[mortberg]

That's cool. What about using intp? not easy to pronounce though.

This might be a reasonable compromise? What I don't like about interp is that my brain will complete it to interpret, not interpolate...

[kangrongji]

Another suggestion: I think mid or midst might be more informative.

[phijor]

I just remembered this PR... It looks like last time, we were all busy bike-shedding names for erp. I'd like to have funExtNonDep and friends in the library though. Could this be rebased and merged?

[pi3js2]

Sorry!

I have renamed the operator to interpolateI, and I also made it private and put it in CartesianKanOps.

[mortberg]

Oops, CI unhappy... Please fix

[pi3js2]

@mortberg so sorry :facepalm: should be better now (make build got past these files locally at least...)

[pi3js2]

Attempted to fix the new CI problem, sorry again.

I am trying to run make check locally but it seems to get stuck for a long time at Cubical.Algebra.Group.GroupPath, I will leave it running. (OOM after 46min :frowning:)

[phijor]

I am trying to run make check locally but it seems to get stuck for a long time at Cubical.Algebra.Group.GroupPath, I will leave it running. (OOM after 46min 😦)

I've checked baf40df locally. Everything still type checks fine.

[pi3js2]

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. :smile:

Unfortunately I am unable right now to run CI checks locally, I hope they will pass...

$ make
make AGDA_EXEC=agda gen-everythings check
make[1]: Entering directory '/home/pi3js2/cubical'
runhaskell ./Everythings.hs gen-except Core Foundations Codata Experiments
agda +RTS -H6G -RTS Cubical/README.agda
Checking Cubical.README (/home/pi3js2/cubical/Cubical/README.agda).
 Checking Cubical.Core.Everything (/home/pi3js2/cubical/Cubical/Core/Everything.agda).
  Checking Cubical.Core.Primitives (/home/pi3js2/cubical/Cubical/Core/Primitives.agda).
  Checking Cubical.Core.Glue (/home/pi3js2/cubical/Cubical/Core/Glue.agda).
   Checking Cubical.Foundations.Prelude (/home/pi3js2/cubical/Cubical/Foundations/Prelude.agda).
agda: Heap exhausted;
agda: Current maximum heap size is 6442450944 bytes (6144 MB).
agda: Use `+RTS -M<size>' to increase it.
make[1]: *** [GNUmakefile:53: check] Error 251
make[1]: Leaving directory '/home/pi3js2/cubical'
make: *** [GNUmakefile:15: build] Error 2

[pi3js2]

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.

[mortberg]

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

[pi3js2]

We changed it so that Foundations.Everything is automatically generated, so no need to edit it manually anymore

Nice! Rebased. :pray: :pray:

[mortberg]

The CI was finally happy so I merged. Thanks for the contribution!