 | This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||
| |||||||||||
Removed section
editI removed the following section, as it seems to do with groupoids and not the fundamental groupoid. (I am not an expert and may be wrong)
In homotopy type theory
edit![[icon]](/wiki/File:Wiki_letter_w_cropped.svg){kind=small} | This section needs expansion. You can help by adding to it. (December 2019) |
In intensional intuitionistic type theory (ITT), types have the structure of weak ∞-groupoids (for details and references, see Homotopy type theory#History). This observation led to the development of homotopy type theory, in which weak ∞-groupoids are a primitive or synthetic notion (meaning they are not defined within the theory).