Maths - Singleton and Contractible Type

Singleton

In 'set', a singleton is a set with one element (its cardinality is 1).

A singleton has the property that every function from it to any arbitrary set is injective.

This concept is not limited to sets, for example, singleton list or 1-tuple.

In computing, there is the unit type. See page here.

In category theory we need to express this concept externally (without looking inside it to see how many elements it has).

for allathere existsx (x=a)

Contractibility of Singletons

This is saying that there is an element 'x' that is equal to every other element of the set. This implies that there is only one element of the set. So how can 'a' potentially represent multiple elements. Perhaps we can work with multiple types of equality and this equality is being imposed externally. So whether a given set is a singleton might depend on the equality used.

This code represents a singleton, it is saying: for a type 'A' and any element of that type 'a' there exists a unique path to a point 'x'.
singl (A : U) (a : A) : U
    = (x : A) * Path A a x

CubicalTT code from here.

This seems quite trivial for conventional set theory. However in HoTT things can get more interesting and this becomes an important concept.

Contractible Type

https://homotopytypetheory.org/2017/09/16/a-hands-on-introduction-to-cubicaltt/

 

Contractibility of Singletons

The following uses notation and ideas from cubical type theory on the page here.

This proves the singleton defined in the code above is contractible.

For a type 'A' and any two elements 'a' and 'b' and a path between those points 'p'.

contrSingl (A : U) (a b : A) (p : Path A a b) :
           Path (singl A a) (a,<i> a) (b,p) =
           <i> (p @ i,<j> p @ i /\ j)

CubicalTT code from here.

This proof produces a path between two singletons like this: diagram contractability of singleton
diagram contractible

This path is a type and to prove it we must construct an instance of the type.

The first component of the above pair has to be a path from a to b, this is what p @ i gives us (note that we are to the right of <i> so that i is now in context). The second component should be a square connecting <i> a to p and this is what the square for p @ i /\ j in this diagram gives us.

 


metadata block
see also:

Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.

 

Terminology and Notation

Specific to this page here:

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2023 Martin John Baker - All rights reserved - privacy policy.