redefine DPath as transport and cleanup proofs

[Alizter]

We redefine DPath as transport. This simplifies many things in the library. We go through and remove many superfluous lemmas and proof steps. I've also simplified various proofs as I've seen fit especially in Smash.v.

[jdchristensen]

This looks great! This will also make it easier to use features of dependent paths even when one is working with transports.

[jdchristensen]

I also noticed that the changes here change the type of dp_concat_p1 from

DPath (fun t : a0 = a1 => DPath P t b0 b1) (concat_p1 p) (dp @Dp 1) dp

to

DPath (fun t : a0 = a1 => DPath P t b0 (transport P 1 b1)) (concat_p1 p) (dp @Dp 1) dp

It's probably worth explicitly writing the type family here (and for nearby results) to the simpler form.

(It also wasn't clear to me what the type of t was when reading these results, so filling this in would help with that as well.)

[Alizter]

@jdchristensen I wasn't able to see the difference in my editor but I will mention that it is the same definitionally. I've gone ahead and added the type annotations now.

[jdchristensen]

LGTM!

[mikeshulman]

Sorry to not notice this before this PR was merged, but I don't think this change is semantically compatible with how we would have to deal with apd in #1868. In fact, the only semantic way I know to make sense of a computing apd in simplicially-based models would instead require changing DPath to be an inductive family with a single "dependent reflexivity" constructor.

[Alizter]

@mikeshulman This PR doesn't actually really change how we define DPath "semantically" just that we use transport in the definition instead. Before this PR it wasn't actually defined as an inductive type, but by path elimination. This is essentially the same as the transport definition, just that before the target type family was a little larger.

I agree that having an "atomic" apd might be necessary if we want definitional computation rules for HITs but I don't see that as an immediate concern. If we do go ahead with defining HITs that way, and we are all reasonably satisfied with the semantics, then we would have to make changes to DPath anyway regardless of whether or not this PR happened.

[jdchristensen]

@mikeshulman Just to make sure I understand: even the previous definition of DPath would not be semantically compatible with how we would have to deal with apd in #1868. But before this PR, it would probably be quite easy to change the definition of DPath to your proposed inductive family, since other places in the library already used conversion functions, so only those conversion functions and basic fact about dependent paths would need to be updated. After this PR, all those conversion functions are gone, so it would be more work to change the definition of DPath.

I guess the question is whether we are going to trying using rewrite rules to make maps from HITs compute on path constructors. On the one hand, having more things compute will certainly save us work, especially when you need to prove things about the proofs that currently use beta rules (and this has been troublesome for me, e.g. in work on joins). On the other hand, adding rewrite rules and changing the definitions of ap and apd would take us further from Book HoTT and further from the hard work that has been done on initiality and semantics which shows that our proofs imply results in models.

[jdchristensen]

@Alizter Our messages crossed, but I think my first paragraph might explain why it might be best to revert this PR (maybe keeping improvements to comments, etc) if we do plan to try #1868. It'll be easier to revert now than later when other changes will interfere.

[jdchristensen]

@Alizter @mikeshulman But maybe I'm wrong about reverting this PR. E.g. if we try #1868, then maybe lots of the things that changed in this PR (e.g. various beta rules for paths) won't be needed at all. (And I definitely like this PR.)

[mikeshulman]

Yes, @jdchristensen's first paragraph was my point. There are three possibilities. This PR changes from the current possibility (A) to a different possibility (B), whereas #1868 would require a third possibility (C), and I suspect that the change from (A) directly to (C) would be easier than from (B) to (C), since (A) is already more opaque.

I'm not sure what my opinion is about whether we should do #1868. If it were up to me, I think I would probably keep things as they are, so that as Dan says this repository could be said roughly speaking to be a formalization of Book HoTT. But personally, I'm not working on this repository much any more -- I'm more invested in HOTT and the new proof assistant for it that I'm developing (where I hope the analogous rules ought to hold definitionally in a less ad hoc way, similar to how they do in cubical type theory) -- and the decisions about this repository should be made by the people who are more invested in it.

[Alizter]

Thanks for your input @mikeshulman, your thoughts are definitely appreciated. I think a change like #1868 won't happen tomorrow. So I'm not particularly worried if we are in (A) or (B) as there seem to be larger concerns with that proposal. So it should be relatively easy work to adapt to an atomic form of DPath if that's what we choose to do.

[jdchristensen]

I'm ok with keeping this PR in place and delaying any decision on #1868 until the future.