Consider (a special case of) cofibration-composition, which for a fixed shape inclusion psi subset chi and any type A produces an equivalence
(chi -> A) -> Sigma ( s : psi -> A ) (chi -> A [ extending s ]).
This equivalence is functorial in the sense that for each f : B -> A, it yields a map of maps from (chi -> B) -> (chi ->A) to Sigma_s (\ chi -> B [extending s]) -> Sigma_s (\ chi -> A [extending s]).
One can say ad hoc what this means in this special case (and probably in every other special case of interest), as I have done with the term cofibration-composition-functorial in #79 .
It would be desirable to:
1) Introduce the general concept of a functorial map and a functorial equivalence. Note that even after making everything in the above description dependent, the general case of cofibration-composition cannot just be expressed directly as such a natural transformation, since the map depends on the choice of an additional piece of data ( the a:\phi -> A). I don't quite know what the most generalized version of functoriality should therefore be; only that my implementation of cofibration-composition-functorial should be an instance of it.
2) There are many other functions in the library which should really be defined as functorial maps. One should add corresponding instances.
The last point might be out of reach at the moment, but I'll add it nonetheless in case anyone has any ideas about it.
3 ) Investigate if a map T A -> S A which is defined for all types A (maybe depending on some additional data d : D(A)) is automatically functorial in A. I suspect this might be true assuming some version of directed univalence. Then one might be able to reduce this question to the corresponding question about natural transformations into the universe (viewed as a Rezk type). If I understand correctly, there one gets naturality for free.
Consider (a special case of)
cofibration-composition, which for a fixed shape inclusionpsi subset chiand any typeAproduces an equivalence(chi -> A) -> Sigma ( s : psi -> A ) (chi -> A [ extending s ]).This equivalence is functorial in the sense that for each
f : B -> A, it yields a map of maps from(chi -> B) -> (chi ->A)toSigma_s (\ chi -> B [extending s]) -> Sigma_s (\ chi -> A [extending s]).One can say ad hoc what this means in this special case (and probably in every other special case of interest), as I have done with the term
cofibration-composition-functorialin #79 .It would be desirable to: 1) Introduce the general concept of a functorial map and a functorial equivalence. Note that even after making everything in the above description dependent, the general case of
cofibration-compositioncannot just be expressed directly as such a natural transformation, since the map depends on the choice of an additional piece of data ( thea:\phi -> A). I don't quite know what the most generalized version of functoriality should therefore be; only that my implementation ofcofibration-composition-functorialshould be an instance of it. 2) There are many other functions in the library which should really be defined as functorial maps. One should add corresponding instances.The last point might be out of reach at the moment, but I'll add it nonetheless in case anyone has any ideas about it.
3 ) Investigate if a map
T A -> S Awhich is defined for all types A (maybe depending on some additional datad : D(A)) is automatically functorial in A. I suspect this might be true assuming some version of directed univalence. Then one might be able to reduce this question to the corresponding question about natural transformations into the universe (viewed as a Rezk type). If I understand correctly, there one gets naturality for free.