search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
211 stars 67 forks source link

Define null-homotopic maps #1136

Open fredrik-bakke opened 1 month ago

fredrik-bakke commented 1 month ago

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 commented 1 week ago

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

fredrik-bakke commented 1 week ago

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