Non-contractible types

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

Created on 2022-08-18.
Last modified on 2024-02-06.

module foundation.noncontractible-types where
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.universe-levels

open import foundation-core.contractible-types
open import foundation-core.empty-types
open import foundation-core.function-types
open import foundation-core.identity-types
open import foundation-core.negation


A type X is noncontractible if it comes equipped with an element of type ¬ (is-contr X).


The negation of being contractible

is-not-contractible : {l : Level}  UU l  UU l
is-not-contractible X = ¬ (is-contr X)

A positive formulation of being noncontractible

Noncontractibility is a more positive way to prove that a type is not contractible. When A is noncontractible in the following sense, then it is apart from the unit type.

is-noncontractible' : {l : Level} (A : UU l)    UU l
is-noncontractible' A zero-ℕ = is-empty A
is-noncontractible' A (succ-ℕ k) =
  Σ A  x  Σ A  y  is-noncontractible' (x  y) k))

is-noncontractible : {l : Level} (A : UU l)  UU l
is-noncontractible A = Σ  (is-noncontractible' A)


Empty types are not contractible

is-not-contractible-is-empty :
  {l : Level} {X : UU l}  is-empty X  is-not-contractible X
is-not-contractible-is-empty H C = H (center C)

is-not-contractible-empty : is-not-contractible empty
is-not-contractible-empty = is-not-contractible-is-empty id

Noncontractible types are not contractible

is-not-contractible-is-noncontractible :
  {l : Level} {X : UU l}  is-noncontractible X  is-not-contractible X
  ( pair zero-ℕ H) = is-not-contractible-is-empty H
is-not-contractible-is-noncontractible (pair (succ-ℕ n) (pair x (pair y H))) C =
  is-not-contractible-is-noncontractible (pair n H) (is-prop-is-contr C x y)

Recent changes