Global goal and plan

[JacquesCarette]

The global README leads me to believe that

Pi combinators ≃ (Fin n ≃ Fin n)

is really the desired end goal. [Though I'd prefer if the latter part was (Fin n ≃ Fin m), where it is understood/provable that for m <> n, the type is empty.] But this issue should be to clearly define the "main message", and then also a plan to get there.

Again, the global README gives a particular plan, via a sequence of equivalences - but nowhere have I seen any reasoning that these particular steps are somehow thought to be the 'easiest' path. [I don't disbelieve it, but neither am I convinced.]

[vikraman]

The end goal is to prove the lemmas in https://github.com/vikraman/2DTypes/blob/master/Pi%2B/Conjectures.agda

There are a few adjustments needed to typecheck the statements. The bit about n == m should show up in the proof there.

[JacquesCarette]

As far as I can see, conjecture ⟦_⟧₁ : {X Y : U} → X ⟷₁ Y → ⟦ X ⟧₀ == ⟦ Y ⟧₀, i.e. line 28-29 of the linked file, is c2equiv on lines 122-148 of https://github.com/JacquesCarette/pi-dual/blob/master/Univalence/PiEquiv.agda (up to univalence, which you seem to employ elsewhere). As a bonus, it's fully constructive.

Conjecture -- ⌜_⌝₁ : {X Y : UFin} → X == Y → ⌜ X ⌝₀ ⟷₁ ⌜ Y ⌝₀ is the really hard one, to me. Even in its constructive form, i.e. with explicit equivalences, it's hard.

Level 2 of the first conjecture ⟦_⟧₂ : {X Y : U} → {p q : X ⟷₁ Y } → p ⟷₂ q → ⟦ p ⟧₁ == ⟦ q ⟧₁ is cc2equiv of the same file (from line 287 onwards). That proves it at the level of symmetric Rig Groupoid, which is much (much) more than you need. There's a couple of bonus coherence theorems after that too.

Having said that, to me the 'key' to the hard conjecture is left-cancel-⊤ in https://github.com/JacquesCarette/pi-dual/blob/master/Univalence/LeftCancellation.agda which is again constructive. This is the key lemma that lets you evaluate a combinator in normal form on the "first component", see where it goes, and tranpose that to be in the head position to recurse. This is indeed 1/2 of the hard part of going from Pi to the Lehmer representation.

Q: does @inexxt get notifications for all issues, or only when explicitly tagged?

[inexxt]

I remember writing something like left-cancel-T a year ago, but can't find it now - but I think the place it was useful was in the proof that Lehmer is equivalent to Aut(Fin n). (definitely have a memory of discussing it with @sabry on a whiteboard - maybe he will remember better?)

I thought about it for quite a bit, and it's difficult for me to comment on the rest. The problem is that the functions in Conjectures.agda are not stand-alone, as higher levels prove things about lower ones etc., so I'm not sure how to integrate - for example - just the finished proofs of c2equiv and cc2equiv - they seem to be in a different paradigm from the "chain of equivalences" I tried to use here. But maybe it is possible to integrate them, and it's just that I don't have that good understanding of the general strategy of pi-dual code.

In my proof, the ⌜_⌝₁ is the easy one - in Coxeter/Group.agda this is immersion, it turns a Lehmer code into a list of transpositions. What is difficult is to show that this is an injection, which is a crucial fact in the definition of ⟦_⟧₁ and later ⟦⌜_⌝⟧₁.

(I do get notifications :))

[vikraman]

A proof of left-cancel is here: https://github.com/vikraman/2DTypes/blob/master/PiFin%2B/Semantics0.agda

[JacquesCarette]

To @inexxt : yes, I agree that it is not straightforward to integrate those functions, they are most easily 'ported' rather than reused, sadly. And c2equiv is not an equivalence, it is 'just' an implementation of ⟦_⟧₁ in the full Rig Groupoid setting. Since the current work only considers the (additive) monoidal aspects, it's considerably shorter. Thanks for pointing me to Coxeter/Group, I had not gotten there (yet). Note that the part that I consider difficult is going from X == Y to a syntactic combinator. At least, when I tried, extracting 'syntactic' information from a X == Y was not clear to me. Of course, part of my difficulty was that I insisted on doing all of it constructively, never allowing any use of any postulate anywhere, nothing that blocked evaluation, etc.

To @vikraman : indeed, reduce-eq is it. More comments in that file would be super-appreciated. In particular, reduce-aux takes a lot of decoding to re-figure out. Note that there is also a proof of something like this in the standard library - and that proof is the cleanest one I've seen. It works hard to "factor out" the patterns in the reduce-η proofs. I do like how you hand-write everything instead of using with. It's also been my feeling that with gets really hard to work with 'at scale'.

[inexxt]

I mean, as far as I understand, we're also doing everything fully constructively here. The postulates that are left in the code are only placeholders, to be filled in later (like these in Arithmetic.agda). The only possible non-constructive thing is univalence axiom, but I don't think we use it anywhere in the proof either (but maybe @vikraman intends to?).