Mike Shulman

I would say that associativity of vector concatenation is a dependent path over associativity of nat addition. But I guess I can see that working with that could be more...

I don't think I've ever heard anyone consider "graded abelian groups" where the gradings belong to a non-hset, if that's what you mean.

Is it not possible to have a single symbol `ap` satisfying rewrite rules for all HITs? Do the rewrite rules for a given symbol have to all be declared at...

Ok, then we could just declare the symbol `ap` along with its rewrite rule for `refl` in `Overture`, and then whenever we introduce a new HIT we give `ap` a...

Oh, okay, I'm surprised. But it should be rare and easy to work around, as you say.

I wonder whether one could prove a conservativity result for a type theory with a primitive `ap` and `apd` and definitional path-constructor computation over ordinary Book HoTT. It feels kind...

(Moving the discussion out of the inline comments on an out-of-date line.) With apologies to Dan who made this suggestion, I don't think this is quite what the exercise means....

Thanks! Sorry that I missed the earlier issue (I was only searching for "coinduction" not "guardedness"). But it looks like 3 years have passed without any progress. If the theoretical...

That sounds promising, I guess. Is anything known about whether a function accepted by any of these termination checkers is in principle expressible using the standard recursors?

That's too bad. Is there *any* known termination-checker that doesn't alter the definitional equalities vis-a-vis the standard recursors? (I don't have a philosophical attachment to recursors, but as far as...