Universal property of smash products

[maybemabeline]

I added some functions for computing with the universal property of pushouts of pointed types and a function that computes the identifications created by the map from the product to the smash product.
I also started working on one of the sides of the universal property, but the last hole ended up as a very complicated dependent identification that I'm not sure how to handle. If anyone wants to look at it, you are welcome to do so :)

[EgbertRijke]

Good work so far! I'd have to write out what you're trying to do, in order to help you, because it's hard to see just like that from a github pull request:) Maybe I'll come up with something over the weekend, if you haven't figured it out by then.

[maybemabeline]

In my latest commit I added some accessors for the first and second projections of equalities in Sigma types. Suggestions for better names for these functions are welcome and please let me know if I missed that these were already implemented somewhere else.

[maybemabeline]

There's some work that still needs to be done with the universal property of the smash product but this pull request is already getting pretty big so I would prefer if this gets merged now and I add the rest in separate pull requests later.

[maybemabeline]

I think removing the brackets doesn't work in the case of pointed maps, because they might not have had the same change of precedence.

[fredrik-bakke]

I think removing the brackets doesn't work in the case of pointed maps, because they might not have had the same change of precedence.

Oh, that is actually an oversight! You have my permission to add the following line to structured-types.pointed-homotopies, right after _~∗_:

infix 6 _~∗_

That should fix the problem.

[fredrik-bakke]

I'll be happy to merge this once the final comments have been addressed. Great work again!

[maybemabeline]

One last thing I'd like get feedback on is on the naming of functions that compute what identifications some function makes, of which I have a few. I realized I've rather awfully variously named them eq-map-smash-prod-wedge-Pointed-Type, inl-glue-smash-prod-Pointed-Type, glue-wedge-Pointed-Type and inl-prod-wedge-Pointed-Type. Would glue-target-source-Pointed-Type be a good general naming scheme, with the prefixes inl- and inr- to differentiate some variants?

[fredrik-bakke]

One last thing I'd like get feedback on is on the naming of functions that compute what identifications some function makes, of which I have a few. I realized I've rather awfully variously named them eq-map-smash-prod-wedge-Pointed-Type, inl-glue-smash-prod-Pointed-Type, glue-wedge-Pointed-Type and inl-prod-wedge-Pointed-Type. Would glue-target-source-Pointed-Type be a good general naming scheme, with the prefixes inl- and inr- to differentiate some variants?

Thanks for asking! I don't think we have a more specialized naming scheme for this than the general one. Some descriptors that are generally used in the context are inl, inr, glue, coh, and compute. As other constructions are introduced, it may be appropriate to introduce names particular to them though.
When considering what descriptor is appropriate, you have to consider what the function of the definition is. Is it to describe glue in a type, or compute glue of a particular map, or to define a coherence between other computations?

[fredrik-bakke]

Thanks again for the fix, looking forward to your next PR! 😊