I could tell that the path algebra was doing something similar to my 
original coerce function, I was just curious how exactly it worked, with 
perhaps a breakdown of what each part is doing, and how you even came up 
with the term in the first place, it seems non-obvious to me, to say the 
very least. Also, I knew that the choice of putting it on the left or the 
right was equivalent, I tried to say as much, but seeing as it aligns with 
what you do in the HIITs paper, I was curious if there was a particular 
reason you seem to prefer the left over the right.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.