Dan Christensen

Interesting idea. Do we expect to have applications? In my non-univalent work with monoidal categories, all diagrams that arose could be factored into the basic commuting regions in a pretty...

I agree with Mike. The coherence really just amounts to cutting a diagram into primitive regions matching the axioms, so it shouldn't rely on univalence.

I think it's good to have classes for various identities. About the direction of associativity: > One thing that has changed is the direction of the associator. We used to...

This is equivalent to having point constructors `sm : X * Y -> Smash X Y` and `aux : Smash X Y`, path constructors `sm x pt = aux` and...

Oh, about naming, I think we most often use names like `functor_join`, `functor_sigma`, `functor_coeq`, etc. (Exceptions are `Trunc_functor` and `O_functor`.) I like the `functor_*` naming, since it also meshes with...

About a lemma for handling the boilerplate, I'm thinking of something like `bundle_joinrecpath` in Join/Core.v. This specifically handles proving that that two functions defined using `join_rec` with definitionally equal point...

I think all of the new proofs would benefit from `pointed_reduce`. About the boilerplate, I mean how every proof uses `Build_pHomotopy`, `Smash_ind`, `reflexivity` for the 2nd and 3rd goals, and...

You need to do `pointed_reduce` with everything in the context, and without manually destructing anything. The following works and is shorter than your proof: ```coq pointed_reduce. snrapply Build_pHomotopy. { snrapply...

> One thing that has been bothering me is that the "recursion data" for smash products seems to use funext in an essential way, whereby you need funext to show...

> after doing the simplifications you suggested I wasn't happy with how slow the Defined was with those changes, so I was hoping for a different way... I had some...