 | This article is rated Start-class on Wikipedia's content assessment scale. It is of interest to the following WikiProjects: | ||||||||||
| |||||||||||
Removed section edit
I 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).