Finish proving braid-transpos (in Level0)

[vikraman]

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

[JacquesCarette]

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]

It might be an application of two hexagons like this.

[JacquesCarette]

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]

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)

[JacquesCarette]

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]

Might be this paper? This is only monoidal though.

[JacquesCarette]

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]

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]

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]

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]

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]

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]

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]

More precisely, I believe it got shifted there:

2DTypes/Pi+/Indexed/Equiv2Hat.agda

Line 114 in dc31270

in s₁ ◎ (id⟷₁ ⊕ s₂) ◎ s₁ ⟷₂⟨ TODO! ⟩

[JacquesCarette]

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]

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 GitHub<#52 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AAWVV2NEUPARA6CZVRI4UTLTDJ7RTANCNFSM4WR6BE2Q>.

[vikraman]

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]

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]

Yes, this injectivity of Fin shows up when defining the univalent subuniverse we're interpreting into:

2DTypes/Pi+/UFin/Univ.agda

Lines 99 to 124 in dc31270

	FinSetUU = SubtypeUU FinSet-prop
	FinSetUU-is-univalent = SubtypeUU-is-univalent FinSet-prop
	FinSet-n-prop : (n : ℕ) → SubtypeProp Type₀ (lsucc lzero)
	fst (FinSet-n-prop n) X = Σ ℕ λ n → Trunc -1 (Fin n == X)
	snd (FinSet-n-prop n) X =
	all-paths-is-prop
	λ { (n , ϕ) (m , ψ) →
	pair= (Trunc-rec (λ p → Trunc-rec (λ q → Fin-inj n m (p ∙ ! q)) ψ) ϕ) prop-has-all-paths-↓ }
	FinSet-n-UU : (n : ℕ) → UU _ _
	FinSet-n-UU n = SubtypeUU (FinSet-n-prop n)
	FinSet-n-UU-is-univalent : (n : ℕ) → is-univalent (FinSet-n-UU n)
	FinSet-n-UU-is-univalent n = SubtypeUU-is-univalent (FinSet-n-prop n)
	BAutUU : (A : Type i) → UU _ _
	BAutUU A = SubtypeUU (BAut-prop A)
	BAutUU-is-univalent : (A : Type i) → is-univalent (BAutUU A)
	BAutUU-is-univalent A = SubtypeUU-is-univalent (BAut-prop A)
	FinSet-exp-is-univalent : (n : ℕ) → is-univalent (BAutUU (Fin n))
	FinSet-exp-is-univalent n = BAutUU-is-univalent (Fin n)
	UFin-is-univalent = FinSetUU-is-univalent

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