Coq-HoTT icon indicating copy to clipboard operation
Coq-HoTT copied to clipboard

replace transportD using transport along path_sigma?

Open mikeshulman opened this issue 11 years ago • 2 comments

Cleaning out my inbox, I found this suggested in an old email thread.

mikeshulman avatar Jun 21 '14 00:06 mikeshulman

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.

Alizter avatar Nov 20 '19 13:11 Alizter

Depends on what you mean by "essentially", I guess. On its face it's about transport, not characterizing dpaths.

mikeshulman avatar Nov 20 '19 14:11 mikeshulman