Polytopes

Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.

Created on 2022-03-12.
Last modified on 2024-09-23.

Modules in the polytopes namespace

module polytopes where

open import polytopes.abstract-polytopes public

Recent changes

• 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
• 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).
• 2023-03-12. Fredrik Bakke and Jonathan Prieto-Cubides. Generate module indexes (#501).
• 2023-03-06. Fredrik Bakke. Remove redundant whitespace in headers (#486).
• 2023-03-03. Jonathan Prieto-Cubides. Hide imports, toc and many other fixes (#480).