Comments (19)
Might be this paper? This is only monoidal though.
from 2dtypes.
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
from 2dtypes.
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.
from 2dtypes.
It might be an application of two hexagons like this.
from 2dtypes.
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.]
from 2dtypes.
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)
from 2dtypes.
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!
from 2dtypes.
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.
from 2dtypes.
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.
from 2dtypes.
Not sure if it helps, but we found this diagram in Joyal&Street paper:
https://www.sciencedirect.com/science/article/pii/S0001870883710558
page 15.
from 2dtypes.
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.
from 2dtypes.
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?
from 2dtypes.
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^
.
from 2dtypes.
More precisely, I believe it got shifted there:
2DTypes/Pi+/Indexed/Equiv2Hat.agda
Line 114 in dc31270
from 2dtypes.
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.]
from 2dtypes.
from 2dtypes.
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
.
from 2dtypes.
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.
from 2dtypes.
Yes, this injectivity of Fin
shows up when defining the univalent subuniverse we're interpreting into:
Lines 99 to 124 in dc31270
But there is some Agda hacking necessary in between to make the cardinalities match up.
from 2dtypes.
Related Issues (20)
- Fix "one generator" to "zero"
- Fix the example with f, g and h HOT 1
- Motivate using HoTT at the beginning
- Add examples to sec 7 to match claims in the introduction
- Fix section 7
- 258: keep notation consistent with ⊚
- Fix the typo "1-loops Aut(Fin n)" on line1025
- Notation for successor and Sn are confusing
- Make a list of claims and their corresponding Agda proofs in a table HOT 1
- Improve HoTT presentation
- Lifting relation on Fin to Fin + Fin
- Explain U+ and U^
- Univalence only needing ua and ua𝛽
- Move the typoid footnote to discussion
- Define fiber and image somewhere in the text
- Typography fixes
- Cite arXiv version and artefact
- Mention previous work with BAut(2) and how this extends it
- Finalize the paper
- Put the full syntax in the appendix
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from 2dtypes.