vikraman/2dtypes

Collaborative work on reversible computing

2DTypes

Collaborative work on reversible computing and its relationship to Homotopy Type Theory. Drafts are available in releases.

2dtypes's Issues

Prove TODO in Level0.agda L166

Normalized subset of Pi+

To do:

• Define normalized types (1 + (1 + ... + (1 + 0))) and normalized 1-combinators
• Show that for any type, there is 1-combinator between it and its normalized version
• Show that for any two types t1 and t2 and a 1-combinator c between them, there exists a normalized 1-combinator nc and a 2-combinator nnc such that the (obvious) diagram commutes up to nnc.

Prove the Coxeter HIT and set quotient versions are equivalent

Compose the equivalences: ∀ n, 1-paths in FSMG.M 1 ≃ Coxeter ≃ LongCoxeter ≃ Lehmer ≃ Aut (Fin n)

Sketch the equivalence between M 1 and UFin

Add text in section 3

Prove postulates in Equiv1Norm.agda

Prove Lehmer is a set

Prove that it is indeed a presentation of Sn

By defining the free group and constructing the surjection, or showing an equivalence between a quotient of Free and the Sn type.

Global goal and plan

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.]

Fix the problem with termination checker in Diamond

There are three functions marked as non-terminating:

• in Pi+/Coxeter/NonParametrized/Diamond.agda: diamond and diamond-full
• in Pi+/Coxeter/NonParametrized/LehmerReduction.agda : Listℕ-to-LehmerProper

All three of them are of similar nature, and they terminate based on the same reason. Namely, when they are called with an argument l1 : Listℕ, they are calling themselves recursively on l2, which has the property that l1 ≅* l2. Relation ≅* has the property that, if l1 ≅* l2, then l2 is lexicographically smaller than l1.

Thus, we need to:

• define the lexicographical order on lists
• construct some mechanism which will be able to call the functions above using this order

Hopefully, this can be done in a generic way, to not bother with the details of the functions above (they are quite messy and I can modify them to fit in the generic interface myself).

Show the univalent sub-universe structure of UFin

Write out the definition of Lehmer code

Show that the 1-combinators in the normalized subset of Pi+ can be expressed as adjacent transpositions.

Prove the equivalence between Coxeter and LongCoxeter

Add text in section 2

Write (or copy) the equivalence Lehmer n ≃ (Fin n ≃ Fin n)

Finish the proof of equivalence between Coxeter and Lehmer

Migrate the proof of equivalence between LongCoxeter and Lehmer

Convert it from Agda std-lib to HoTT.

Show that UFin is a symmetric monoidal groupoid

Write the two definitions of FSMG and assert their universal properties

Finish proving braid-transpos (in Level0)

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

Show that FSMG.M is a symmetric monoidal groupoid

Fill in Conjectures

Some stuff will still be missing, but just to see where we are now and what's still to be done.

Construct the quotient of List (Fin n) by the Coxeter relation

This requires that the Coxeter relation:

• is an equivalence
• is prop valued (diamond lemma)

Taskboard for MFPS submission

• Sec 1
• Sec 2
• Sec 3 ( @vikraman )
  • Univalent fibrations
  • Propositional Truncation
  • Univalent sub-universes
  • U[2] is univalent
• Sec 4 ( @DreamLinuxer )
  • Write down the proofs in literate agda?

Prove the universal property of FSMG.M

Taskboard for TYPES 16 POSTPROCEEDINGS submission

• Write Introduction
• Remove/update section 3.6
• Change the name "division groupoid"
• Better name for Prim⟷?
• Change syntax for 𝓐𝓹 (@DreamLinuxer doesn't want it)
• in 2D/Frac.agda, I currently defined "left groupoid" and "right groupoid", corresponding to // and \ more closely. The symmetric definition worked, but was really not justified. I think these are easier to explain. If you agree, I can tweak section 3.5 accordingly. But that does give us left and right division groupoids, which will mean that Pi will need adapted. I don't think that will take too long.
• Proof sketch of lemma 7
• In 4.1, remove all mention of information
• In 4.1, // and \\ and # are not 'convenience'!
• In 4.1, explain more deeply why we're influenced by compact closed categories (ccc from here on).
• In 4.1, explain that we need to introduce fractions, so from ccc we go with generalizations of 1 = a/a, which then show up in 2 pairs.
• in 4.1, explain that the ccc associativity A x (A* x A) ~ (A x A*) x A is not fine enough. In our situation, this shows up as #p x (q \ p) ~ (p // q) x #p. We call them 'synchr' from the effect they have in the operational semantics, even though these are induced by an associativity axiom. And not a commutativity axiom, even though that's what the syntax makes it look like!
• In 4.1, try to hide all the parts of the definitions which have already been seen, to focus on just the new ones. And explain a lot.
• in 4.2, introduce left and right-handed versions of 'division'. Use as appropriate in tangle.
• in 4.2, explain that 'tangle' as a name is chosen because of the op.sem.
• in 4.2, should prove a handed-version of lemmas at the end. And find a cleaner way to state them - the current way is quite ugly.
• 5 should be split into sections (op.sem., properties, examples)
• in 5.1, the definition of the action of synchr seems naive, but in the code I (JC) proved some structure lemma that says that this is the only choice. Comment.
• in 5.1, there should be a lot more explanations throughout.

Deal with the transports in Equiv1.agda

Write down all the types and theorems with postulates

Prove the group structure of CList

Sketch a first draft of the paper

Prove the equivalence of UFin paths and Aut (Fin n)

Update the conjectures for equivalence between Pi and UFin

Is Lemma 5.1 of "Categories of Petri Nets" somehow relevant

https://arxiv.org/abs/2101.04238. It's about the free symmetric strict monoidal category.

Add text in section 4

Prove the base case

Show that for any (p : O ⟷₁ O) → (id⟷₁ ⟷₂ p).

Finish writing the conjectures between Pi.U and UFin

Prove eval (quote X) == X for level 0

Setup a CI which typechecks the main theorems/conjectures

Prove the symmetric monoidal laws for Fin n with coproduct

Prove eval₂

Prove quote-eval^₁

Decide between FinSet vs FinSet-exp

Maybe we could use FinSet-exp instead of FinSet? The latter is very inconvenient to use because of its monadic form?

Setup HoTT-Agda with 2.6.1 and bootstrap

Document required Agda version

I'm attempting to build the project, but am encountering syntax errors both with Agda 2.5.2 and git HEAD (agda/agda@01798f3). Is there any chance that the Agda version needed could be noted somewhere, even if just as a comment in the Makefile?

Write the equivalence between path space of `FSMG 1` and Coxeter

Write out the definion of Coxeter relation as a HIT

Prove quote-eval^₁

Prove the universal property of FSMG

Partially done in FSMG.Properties