some paths in sigma type
pointed lift/lower
name the ptd-span that produces a suspension
transporting pointed functions