Define null-homotopic maps

[fredrik-bakke]

Defines null-homotopic maps and characterizes their equality. In particular, a sufficient condition for when being null-homotopic is a property is given.

[fredrik-bakke]

I'm briefly marking this PR as a draft to add a computation.

[fredrik-bakke]

We can also consider calling null-homotopic maps "constant" and then refer to constant maps as "standard constant maps".

[VojtechStep]

LGTM, if you pull in master I'll merge it 👌