Indexed datatype in definition of free categories.

[marcinjangrzybowski]

I plan to use definitions from #666 for some development.
But definition Path
uses indexed datatype to define paths.

There were some issues with indexed datatypes in cubical agda mentioned in the past here and there, so I want to ask if I can expect such definition to be compatible with cubical machinery?
I can imagine doing this with Parametrized datatype, by adding necessary equations to the constructors. Is there any reason to believe that such additional bookkeeping may somehow pay off by better evaluation of expression with lots of Glue and transport? Or Is this only going to move complexity somewhere else?