Coq-HoTT
Coq-HoTT copied to clipboard
replace transportD using transport along path_sigma?
Cleaning out my inbox, I found this suggested in an old email thread.
This is essentially about characterizing dependent paths over sigmas right? I tried this a while back and got very stuck. I would have heuristically guessed something like "DPaths between sigmas" are "sigmas of dpaths". But making this precise is a bit tricky.
Depends on what you mean by "essentially", I guess. On its face it's about transport, not characterizing dpaths.