search

vikraman / 2DTypes

Collaborative work on reversible computing
17 stars 1 forks source link

Finish proving braid-transpos (in Level0) #52

Closed vikraman closed 3 years ago

vikraman commented 3 years ago

It looks like a hexagon but it doesn't match any existing pi combinators?

JacquesCarette commented 3 years ago

I'm going to guess that it is, but that one needs to first shuffle things into place. Our combinators might be 'wrong-handed' (syntactically), but a combination of what is there imply what is needed.

vikraman commented 3 years ago

It might be an application of two hexagons like this. image

JacquesCarette commented 3 years ago

That would be rather sneaky, wouldn't it? Hmm, I'm not quite seeing the relation between the two diagrams though.

What I'm seeing on the left reminds me of some quantum circuit equivalences that are only true when the X exists, but not derivable otherwise. We can just add a + X to the rhs diagram to make it look like the one on the left...

I'm guessing that you have more in your head than what you're communicating here, so that I'm not quite able to bridge the gap. [And I have not had a chance to play with it yet, it might be obvious if I did. But not today, unfortunately.]

vikraman commented 3 years ago

It is basically this diagram from the last step in Maclane's proof, except there he collapses the hexagons to triangles by forcing the assoc/units to identities, so we have to work out the proof relevant version of this. (My previous diagram isn't correct)

image

JacquesCarette commented 3 years ago

Ah indeed. Very helpful. I was going to look at some of the proofs of Maclane's coherence theorem - I think Dybjer's paper might skip fewer details. If only I could remember the title of that paper!

vikraman commented 3 years ago

Might be this paper? This is only monoidal though.

JacquesCarette commented 3 years ago

Aha - https://www.researchgate.net/publication/227308222_Extracting_a_proof_of_coherence_for_monoidal_categories_from_a_proof_of_normalization_for_monoids . Also, there might be useful material in this nLab page

JacquesCarette commented 3 years ago

I've spent multiple hours, using pen and paper, to scribble many many things, to no avail. I've tried from both ends of what is being asked, and nothing goes. I mean, lots and lots of rewrites are possible, but none of them make things get any closer.

In particular, in the hole, and derived things from that, there is nothing quite like that diagram (i.e. the outer edge compositions). The issue seems to be that the ' . 1' on the right in the above (which is + Id in our case) just isn't there in what we're asked to prove by Agda.

JacquesCarette commented 3 years ago

Hmm, I've had a couple more ideas of things to try. One weird thing some of the coherence proofs do (for the pure monoidal case) is to introduce some unitors "in the middle", only to eliminate them later. I had definitely not done that. Plus I've spotted a use of the pentagon equation that I had not considered in that shape.

Maybe what I first need to do is to prove the above 'last step' formally, as a warm-up.

inexxt commented 3 years ago

Not sure if it helps, but we found this diagram in Joyal&Street paper: https://www.sciencedirect.com/science/article/pii/S0001870883710558 page 15.

JacquesCarette commented 3 years ago

It surprisingly doesn't - I had re-derived that one multiple times while noodling around.

The problem is the 'outer' (Id +). (Id + swap) is great, (Id + c) for c some non-trivial combinator expression, not so much.

I'm starting to wonder if the problem might be that the proof at the lower-level is the problem. I wouldn't think that it's wrong, just that it is not coherently chosen to fit with the rest. I suspect that it is too specialized to the case of having 1 as a type, instead of being fully polymorphic.

JacquesCarette commented 3 years ago

So if I'm reading the diffs properly, in the new encoding braid-transpos^ is what solves this? It now looks so 'easy'! What was the key idea?

vikraman commented 3 years ago

I think there have been many changes since this diff. We're now working with an indexed version of the syntax (indexed by the cardinality), and further we've defined Pi^ which is a normalised version of Pi syntax. We can show that Pi^ is complete wrt the semantics, and now we're trying to prove the equivalence between Pi and Pi^. The braid-transpos^ is the corresponding lemma for Pi^ which is simpler to prove, but the hexagon problem just got shifted somewhere else in the equivalence between Pi and Pi^.

inexxt commented 3 years ago

More precisely, I believe it got shifted there: https://github.com/vikraman/2DTypes/blob/dc312705283c0c61ddf2a7d12ffa201289833da7/Pi%2B/Indexed/Equiv2Hat.agda#L114

JacquesCarette commented 3 years ago

I had indeed noticed that there had been very major changes. But, as a now completely outside onlooker, I'm still quite interested in trying to understand. And it didn't seem like this obligation would disappear - and indeed it has not, just moved.

Indexing by the cardinality is indeed a nice idea. I guess since you're using HoTT, you have use just one and a bunch of transports to tweaks the types. [If you use 2, no transports are needed at all, which I personally find more appealing.]

sabry commented 3 years ago

Ah you’re saying we should try to index by two numbers… we’ve been having problems with transports. Vikraman and Jacek, is that worth trying or are we too far along the other path :-) ? —Amr

On Mar 12, 2021, at 17:11, Jacques Carette @.**@.>> wrote:

I had indeed noticed that there had been very major changes. But, as a now completely outside onlooker, I'm still quite interested in trying to understand. And it didn't seem like this obligation would disappear - and indeed it has not, just moved.

Indexing by the cardinality is indeed a nice idea. I guess since you're using HoTT, you have use just one and a bunch of transports to tweaks the types. [If you use 2, no transports are needed at all, which I personally find more appealing.]

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/vikraman/2DTypes/issues/52#issuecomment-797785809, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAWVV2NEUPARA6CZVRI4UTLTDJ7RTANCNFSM4WR6BE2Q.

vikraman commented 3 years ago

Not sure if I follow, types are indexed by one number, combinators are indexed by two numbers.

The transport appears when moving from combinators to words in Sn, we have to pick a natural number, so we use a helper lemma to say that n <--> m implies n == m and then use n.

JacquesCarette commented 3 years ago

I think it is now conventional wisdom that permutations (at least in dependent type circles) is an isomorphism between Fin n and Fin m, and a provable theorem that n = m. And isos are between a type A and a type B - and there is no a priori reason that these have to be of the same size. It's again a theorem that they are.

(Just saw @vikraman 's reply as I was typing). Indeed, at the point where you go to Sn, you need transport, it is inevitable.

vikraman commented 3 years ago

Yes, this injectivity of Fin shows up when defining the univalent subuniverse we're interpreting into: https://github.com/vikraman/2DTypes/blob/dc312705283c0c61ddf2a7d12ffa201289833da7/Pi%2B/UFin/Univ.agda#L99-L124

But there is some Agda hacking necessary in between to make the cardinalities match up.