# Maths - Shapes

Here are some ways of modeling various Shapes:

Homotopy Type As Cell Complex
Circle
n-sphere
Torus
Möbius Band
Projective Space
kleinBottle

### N-Sphere

Here is more detail about constructing the n-sphere using paths.

 0-sphere 1-sphere 2-sphere 3-sphere and so on... The 0-sphere consists of 2 points. There is no non-trivial structure for higher dimensions. The circle (1-sphere) consists of: 2 points. and 2 lines between these points. There is no non-trivial structure for 3D and above. The hollow sphere (2-sphere) consists of: 2 points. 2 lines between these points. and 2 planes between these lines. There is no non-trivial structure for 3D and above.
 Could the circle be constructed using just one base point and one line?

### Contractibility of Singletons

 This code represents a singleton, it is saying: for a type 'A' and an element of that type 'a' there exists a unique path to any point 'x'. ```-- "contractibility of singletons": singl (A : U) (a : A) : U = (x : A) * Path A a x``` CubicalCC code from here. This proves it 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, a) (b,p) = (p @ i, p @ i /\ j)``` CubicalCC code from here. ```-- The first component of the above pair has to be a path from a to b, -- this is exactly what p @ i gives us (note that we are to the right -- of so that i is now in context). The second component should be -- a square connecting a to p and this is exactly what the above -- square for p @ i /\ j gives us```