Auto-paper generator

[jamievicary]

Globular should be able to generate an entire research paper from a workspace, in the following way.

• First, cells are sorted in logical order corresponding to their dependencies --- i.e., if cell A depends (directly or indirectly) on cell B, then it is listed after cell B.
• For each statement & proof pair, a new lemma is created (i.e. "\begin{lemma} ... \end{lemma}"), whose statement and proof embeds the appropriate sequences of diagrams.
• Generators not part of such a pair are given as defintions (i.e. "\begin{definition} ... \end{definition}"), the content of which is the appropriate sequence of pictures.
• Links to the online version are automatically embedded, with codes so that the correct theorem is displayed automatically.
• Extra descriptive text associated to a cell is automatically used for statements of definitions and theorems, and in the bodies of proofs.

I imagine clicking a single button and this entire structure being created and downloaded automatically as a zip file, containing a .tex file and a collection of graphics. The resulting .tex file would then form the basis for a "real" research paper, which the user would edit directly.

[cdgls]

I think the following should be the standard method for displaying outputs.

By default, a cell that is not a composite is output as follows:

Cell of dimensions 0-2 is an unprojected single picture Cell of dimension 3 is a movie (of length 2) of 2d unprojected pictures Cell of dimension 4 is a movie (of length 2) of movies of 2d unprojected pictures Cell of dimension 5 is a movie (of length 2) of movies of 2d 1-projected pictures Cell of dimension 6 is a movie (of length 2) of movies of 2d 2-projected pictures etc.

By default a cell that is a composite is output as follows: Cell of dimension 1-2 is an unprojected single picture Cell of dimension 3 is a movie of 2d unprojected pictures Cell of dimension 4 is a movie of 2d 1-projected pictures Cell of dimension 5 is a movie of 2d 2-projected pictures etc.

The principle here is that only the unprojected pictures contain all the information, so should be used as long as possible before beginning to project. (Subject to the principle that large (both sides of length > 1) movies of movies are hard to interpret, but elementary movies of length 2 x n are okay, since we read them as a single transition between movies we understand.)

---

The above is the default, but if a cell is typed, the output can be improved as follows:

Axioms: All axioms are displayed as the above default for noncomposite cells, in a single definition: \begin{def} Let C be the free 4-category with the following generators and relations: 0-dimensional generators:

1. [the first zero cell]
2. [the second zero cell] 1-dimensional generators: etc \end{def}

NamedCells/Definitions: The pair of a named cell and a definition results in a single definition: \begin{def} NamedCell [displayed as the above default for noncomposite cells] is defined to be Target(Definition) [displayed as the above default for composite cells]

Theorems/Proofs: The pair of a theorem and proof results in a single output: \begin{thm} The cell Source(Theorem) [displayed as the above default for composite cells] is equivalent/equal to Target(Theorem) [displayed as the above default for composite cells] \end{thm} \begin{proof} Slice1(Target(Proof)) [displayed as the above default for composite cells] Slice2(Target(Proof)) [displayed as the above default for composite cells] etc \end{proof}

---

Notice this actually gives a pretty good situation. Assume that we are working with globular 4-categories, so the theorems are 5-cells and the proofs are 6-cells. But Target(Proof) is then a 5-cell, and Slice1(Target(Proof)) is a (composite) 4-cell, which is then displayed as a movie of 2d 1-projected pictures. In practice, I think this is the project that conveys the information about what is happening best, for the sorts of examples we've been looking at.

(Though it's certainly possible that what's best is application dependent, so one might want ways of telling globular how to change the amount of projection in the outputs.)

Also, this will all shift of course once the 3d display is up and running.

[jamievicary]

This is great! Of course before this can be practical we need LaTeX output for graphics.

On Tue, May 3, 2016 at 7:33 PM, cdgls notifications@github.com wrote:

I think the following should be the standard method for displaying outputs.

By default, a cell that is not a composite is output as follows:

Cell of dimensions 0-2 is an unprojected single picture Cell of dimension 3 is a movie (of length 2) of 2d unprojected pictures Cell of dimension 4 is a movie (of length 2) of movies of 2d unprojected pictures Cell of dimension 5 is a movie (of length 2) of movies of 2d 1-projected pictures Cell of dimension 6 is a movie (of length 2) of movies of 2d 2-projected pictures etc.

By default a cell that is a composite is output as follows: Cell of dimension 1-2 is an unprojected single picture Cell of dimension 3 is a movie of 2d unprojected pictures Cell of dimension 4 is a movie of 2d 1-projected pictures Cell of dimension 5 is a movie of 2d 2-projected pictures etc.

The principle here is that only the unprojected pictures contain all the information, so should be used as long as possible before beginning to project. (Subject to the principle that large (both sides of length > 1) movies of movies are hard to interpret, but elementary movies of length 2 x n are okay, since we read them as a single transition between movies we

understand.)

The above is the default, but if a cell is typed, the output can be improved as follows:

Axioms: All axioms are displayed as the above default for noncomposite cells, in a single definition: \begin{def} Let C be the free 4-category with the following generators and relations: 0-dimensional generators:

1. [the first zero cell]
2. [the second zero cell] 1-dimensional generators: etc \end{def}

NamedCells/Definitions: The pair of a named cell and a definition results in a single definition: \begin{def} NamedCell [displayed as the above default for noncomposite cells] is defined to be Target(Definition) [displayed as the above default for composite cells]

Theorems/Proofs: The pair of a theorem and proof results in a single output: \begin{thm} The cell Source(Theorem) [displayed as the above default for composite cells] is equivalent/equal to Target(Theorem) [displayed as the above default for composite cells] \end{thm} \begin{proof} Slice1(Target(Proof)) [displayed as the above default for composite cells] Slice2(Target(Proof)) [displayed as the above default for composite cells] etc

\end{proof}

Notice this actually gives a pretty good situation. Assume that we are working with globular 4-categories, so the theorems are 5-cells and the proofs are 6-cells. But Target(Proof) is then a 5-cell, and Slice1(Target(Proof)) is a (composite) 4-cell, which is then displayed as a movie of 2d 1-projected pictures. In practice, I think this is the project that conveys the information about what is happening best, for the sorts of examples we've been looking at.

(Though it's certainly possible that what's best is application dependent, so one might want ways of telling globular how to change the amount of projection in the outputs.)

Also, this will all shift of course once the 3d display is up and running.

— You are receiving this because you authored the thread. Reply to this email directly or view it on GitHub https://github.com/jamievicary/globular/issues/29#issuecomment-216623128