Contractible Types Properties

1. Contractible Properties

1 Contractible Properties

module Lib.Prop.Contr where

This file regroups properties of contractible types and maps not provided by the standard library.

1.1 Packages imports

The imported packages can be accessed via the following links:

import Stdlib.Prelude
import Lib.Prop.Paths
import Lib.Prop.Σ

1.2 Accessors

center (A : U) (c : is-contr A) : A =
  c.1

contraction (A : U) (c : is-contr A) : (x : A) → Path A (center A c) x =
  c.2

1.3 Contractibility of Σ_{x: A}(a = x)

In this section, we show that Σ (a₁ : A) (a₀ = a₁) is contractible.

Indeed, the center of contraction is (a₀, refl).

is-contr/Sg-path-center (A : U) (x : A) : Σ A (λy. Path A x y) =
  (x, refl A x)

In turn, the contraction is immediate by sigma-induction and path-induction.

is-contr/Sg-path-contr (A : U) (x : A) (v : Σ A (λy. Path A x y))
                          : Path (Σ A (λy. Path A x y)) (is-contr/Sg-path-center A x) v =
  let B : A → U = (λy. Path A x y)
      u : Σ A B = (is-contr/Sg-path-center A x)
  in
  ind-Σ A B (λz. Path (Σ A B) u z)
             (λy q. J A u.1 (λy' r. Path (Σ A B) u (y', r))
                            (SgPathO→PathΣ A B u u (refl A u.1, PathO/refl A u.1 B u.2 u.2 (refl (B u.1) u.2)))
                      y q) v

Thus, this space is contractible.

is-contr/Sg-path-is-contr (A : U) (x : A) : is-contr (Σ A (λy. Path A x y)) =
  (is-contr/Sg-path-center A x, is-contr/Sg-path-contr A x)

1.4 Contractible `A` implies fiber inclusion equivalence

We show that if A is contractible, then if a : A is its center of contraction, the map B a → Σ A B is an equivalence.

Sg/left-unit-law-is-contr/map (A : U) (B : A → U) (c : is-contr A) (a : A) : B a → Σ A B =
  λb. (a, b)

Sg/left-unit-law-is-contr/inv-map (A : U) (B : A → U) (c : is-contr A) (a : A) : Σ A B → B a =
  λt. tr A t.1 a (comp A t.1 c.1 (inv A c.1 t.1 (c.2 t.1)) a (c.2 a)) B t.2

Sg/left-unit-law-is-contr/right-htpy (A : U) (B : A → U) (c : is-contr A) (a : A)
                                        : Htpy' (Σ A B) (Σ A B) (λt. Sg/left-unit-law-is-contr/map A B c a (Sg/left-unit-law-is-contr/inv-map A B c a t)) (id (Σ A B)) =
  λt. SgPathO→PathΣ A B (Sg/left-unit-law-is-contr/map A B c a (Sg/left-unit-law-is-contr/inv-map A B c a t)) t
    (inv A t.1 a (comp A t.1 c.1 (inv A c.1 t.1 (c.2 t.1)) a (c.2 a)),
     tr/left-inv A B t (Sg/left-unit-law-is-contr/map A B c a (Sg/left-unit-law-is-contr/inv-map A B c a t)) (comp A t.1 c.1 (inv A c.1 t.1 (c.2 t.1)) a (c.2 a)))

Sg/left-unit-law-is-contr (A : U) (B : A → U) (c : is-contr A) (a : A) : retract-of (Σ A B) (B a) =
  (Sg/left-unit-law-is-contr/inv-map A B c a, (Sg/left-unit-law-is-contr/map A B c a, Sg/left-unit-law-is-contr/right-htpy A B c a))

1.5 Contractibility is closed under Σ types

Sg/is-contr (A : U) (B : A → U) (is-contr-A : is-contr A) (is-contr-fam : ((x : A) → is-contr (B x)))
               : is-contr (Σ A B) =
  is-contr/closed-retract
    (Σ A B)
    (B (center A is-contr-A))
    (Sg/left-unit-law-is-contr A B is-contr-A (center A is-contr-A))
    (is-contr-fam (center A is-contr-A))

Sg/is-contr' (A : U) (B : A → U) (is-contr-A : is-contr A) (a : A) (is-contr-B : is-contr (B a))
                : is-contr (Σ A B) =
  is-contr/closed-retract
    (Σ A B)
    (B a)
    (Sg/left-unit-law-is-contr A B is-contr-A a)
    (is-contr-B)

1.6 If `A` is contractible, any two of its elements are equal

is-contr/all-elements-equal (A : U) (c : is-contr A) (x y : A) : Path A x y =
  comp A x
    ( center A c)
    ( inv A (center A c) x (contraction A c x))
    y (contraction A c y)

Contractible Types Properties

Table of Contents