issues
search
UniMath
/
agda-unimath
The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
219
stars
70
forks
source link
Some results about path-cosplit maps
#1167
Open
fredrik-bakke
opened
1 month ago
fredrik-bakke
commented
1 month ago
When the domain is $n+r+2$-truncated the type of $n$-path-cosplittings is $r$-truncated
When the domain is $n+1$-truncated $n$-path-cosplittings are unique
When the domain is $n$-truncated there are unique $n$-path-cosplittings
path-cosplittings are closed under path-cosplit morphisms of arrows
path-cosplittings are closed under equivalences of arrows
path-cosplittings are closed under homotopies
3-for-2 of path-cosplittings
products of path-cosplittings
total space path-cosplittings
dependent products of path-coplittings
coproducts of path-cosplittings