Contractibility

This is a literate Rzk file:

#lang rzk-1

Definition 3.11.1

A type \(A\) is contractible, or a singleton, if there is \(a : A\), called the center of contraction, such that \(a = x\) for all \(x : A\). We denote the specified path \(a = x\) by \(\mathsf{contr}_{x}\).

#define isContr
  ( A : U)
  : U
  := Σ (a : A) , (x : A) → a = x

#define center
  ( A : U)
  : isContr A → A
  := \ (a , _) → a

#define contr
  ( A : U)
  ( isContr-A : isContr A)
  ( x : A)
  : center A isContr-A = x
  := second isContr-A x