PDF cleanup: explain sigma and pi types

[williamdemeo]

Description

This addresses a couple of items of #258

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

[WhatisRT]

I think we don't have any dependent types in the PDF (and if we do we should get rid of them), so I see no reason to include this in the PDF.

[williamdemeo]

Shouldn't we at least explain Σ, which does appear in the PDF?

[WhatisRT]

No, we should get rid of them (except if they denote summation)

[williamdemeo]

I'm resurrecting this PR that was rejected when it was initially created over a year ago. Perhaps, in its current state, the explanations here are too detailed even for an appendix. However, it was recently suggested that we should, in fact, explain Sigma types at least, so we might find some of this PR useful.

[WhatisRT]

I'm closing again this because we first need to have a discussion, which I made #691 for and which links to this PR. It can be reopened if the decision is to keep these in the PDF.