Content created by Egbert Rijke and Fredrik Bakke.
Created on 2023-04-26.
Last modified on 2023-04-26.
The plus-principle asserts that any acyclic 1-connected type is contractible.
plus-principle : (l : Level) → UU (lsuc l) plus-principle l = (A : UU l) → is-acyclic A → is-connected one-𝕋 A → is-contr A
- 2023-04-26. Egbert Rijke and Fredrik Bakke. Acyclic maps (#565).