The plus-principle

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-26.
Last modified on 2023-10-22.

module synthetic-homotopy-theory.plus-principle where
Imports 
open import foundation.connected-types
open import foundation.contractible-types
open import foundation.truncation-levels
open import foundation.universe-levels

open import synthetic-homotopy-theory.acyclic-types

Idea

The plus-principle asserts that any acyclic 1-connected type is contractible.

Definition

plus-principle : (l : Level) → UU (lsuc l)
plus-principle l =
  (A : UU l) → is-acyclic A → is-connected one-𝕋 A → is-contr A

Recent changes