Define section-retraction pairs. Show that in such a pair, the section is an equivalence iff the retraction is an equivalence. (This is essentially a synonym of is-equiv-left-factor and is-equiv-right-factor with a different signature.)
Define free path space and show that the canonical map A -> free-paths A is an equivalence.
Collect three different versions of the arrow type under a common heading in 05-segal-types.
Define section-retraction pairs. Show that in such a pair, the section is an equivalence iff the retraction is an equivalence. (This is essentially a synonym of
is-equiv-left-factor
andis-equiv-right-factor
with a different signature.)Define free path space and show that the canonical map
A -> free-paths A
is an equivalence.Collect three different versions of the arrow type under a common heading in
05-segal-types
.