A1-shape of the universe is contractible

[felixwellen]

Write down a proof that the map from the universe to its $\mathbb{A}^1$-shape is constant. Use that: For types A,B a line in $\mathcal{U}$ parametrized by $x:\mathbb{A}^1$ can be constructed in the following ways (using $0\neq 1$): (joint idea with @MatthiasHu )

[felixwellen]

The argument also applies to the type of $\mathbb{A}^1$-modal types. Using the first variant of constructing the line, it also extends to types of structured types like R-modules.

[felixwellen]

This is by now written down as example 1.0.5 in the draft on A1-homotopy theory -> closing.