🚰 filler-of tactical?

[cangiuli]

(from a discussion with @favonia and @TOTBWF)

We often define operations on paths (such as symm) by composition/coercion to 0 or 1, but as soon as we want to prove any laws about those operations, we have to define and reason about the corresponding filler (symm-filler). @favonia suggested defining a filler-of tactical that returns the filler of any composite, e.g., if foo produces hcom A 0 1 {...} {...}, then filler-of foo produces i => hcom A 0 i {...} {...}.

This is an alternate solution to #179.

[favonia]

VERY SERIOUS ISSUE: Should the Unicode version be 🚰? (Or maybe ⛽? I like 🚰 more.)

[jonsterling]

So personally i kind of preferred the other approach from the other ticket, but with that said, i think this is a fine idea that we could implement.

[cangiuli]

What I like about this approach is that we don't need to bind and possibly even export two names for every operation like symm and symm-filler. But both ideas just involve writing a fancy tactic, so there's no reason (except for inconsistent style) not to try both if we have the bandwidth.

[jonsterling]

What seems quite broken about it is that you cannot easily tell, up to definitional equality, that something is actually an hcom and extract the composition problem from it. So it seems like you are planning some subequational tool if i understand correctly, but that seems way to brittle to consider…

…

On Thu, Jul 29, 2021, at 10:57 AM, Carlo Angiuli wrote: What I like about this approach is that we don't need to bind and possibly even export two names for every operation like `symm` and `symm-filler`. But both ideas just involve writing a fancy tactic, so there's no reason (except for inconsistent style) not to try both if we have the bandwidth. — You are receiving this because you commented. Reply to this email directly, view it on GitHub <#259 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAANOEL34BWCDJD42F4Z64TT2GJBLANCNFSM5AKHYGCA>.

[cangiuli]

After discussing with @jonsterling, we agreed that the best way to implement this feature is to build on #179.

Suppose we define symm as an hcom 0->1 using the abstract hcom mechanism from #179; then symm A p will compute to fresh-hcom-7 A p 1 where fresh-hcom-7 is an opaque global definition (possibly with some special flag?) that cannot be named by the user. Then we can implement filler-of to turn the above neutral application into i => fresh-hcom-7 A p i.