# Start a new discussion

## Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

## Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

1. copying page from HoTT wiki

Anonymous

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeJun 9th 2022

Just to say that I have been using the titles of the form XYZ -- references as !include-files, meaning that in some other entries they are being included with the code

[[!include XYZ -- references]]


For example, in the entry homotopy type theory you see a section References – Homotopy theory formalized in homotopy type theory.

If you look at the pages source code (here) you see that this entire section appears as a single line

[[!include homotopy theory in homotopy type theory -- references]]


The actual content of the section is at

which is an entry that is not necessarily meant to be viewed stand-alone.

Anyways, that’s just to indicate how I have been using this.