UniMath/TypeTheory

A formalisation of the mathematical study of type theories, in the setting of univalent foundations.

Browsable html versions of the development:

• master branch: TOC, index. (Note: not automatically updated; please alert maintainers if this has become stale.)
• tag 2017-ALV1-arxiv: TOC, index
• tag 2017-displayed-cats-arxiv: TOC, index
• tag 2017-displayed-cats-fscd: TOC, index
• tag 2017-displayed-cats-arxiv-v2: TOC, index