Lemma 2.1.2. Concatenation of paths

[IanRay11]

In the 'first proof' of this lemma the following is stated

Here it is said, "We will instead define a function with the equivalent type...". What exactly is the intended meaning of equivalence here?

I'm assuming logically equivalent is what is intended because we are interpreting the type as a proposition. If this is the case, I think because a distinction was made between the two notions of equivalence in chapter 1 we should respect the distinction here.

If I am mistaken and what is intended is the yet to be introduced notion of equivalence of types I think further comments need to be made. Although I am not yet familiar enough with this notion to make further suggestions on what should be said.

[mikeshulman]

Hah, you caught us trying to sneak something past. Actually what's meant here is "judgmentally isomorphic", i.e. there are functions in either direction between these two types and the round-trip composites in either direction are judgmentally equal to identities. It's basically a fancy version of commuting the arguments of a function, turning A -> B -> C into B -> A -> C.

[IanRay11]

Ahhhh, I see. I assume this notion is discussed further in either Chapter 3 Sets and Logic or Chapter 4 Equivalences?

My real issue is the lack of assurance that inhabiting the "equivalent" type is sufficient to inhabit the type that naturally represents the proposition. I'm assuming that the maps back in forth in either direction takes care of this concern.

[mikeshulman]

I don't think the notion of "judgmentally isomorphic" is really discussed in the book. It's kind of a technical device.

Perhaps the proof here should just observe that there is a function from the second type to the first, and therefore to inhabit the first it suffices to inhabit the second. And maybe remark in passing that in fact these two types are "equivalent" in the sense to be discussed later and even a stronger one, but we don't need that.

[IanRay11]

Yes. I think that would be fine. I have just convinced myself that the two are logically equivalent (functions going both ways as defined earlier). But your point about only needing the function from the second to the first is astute.