Post #1816223

@dwarn I have so far failed to come up with an alternative proof showing that there is an Id-collapsible map on the type. Now that I see your solution as a formalization of a homotopical proof maybe thinking about loop spaces is essential.