Re: [HoTT] "Identifications" ?

[Michael Shulman <shu...@sandiego.edu>]

The word "path" is closely tied to the homotopy interpretation, and to
the classical perspective of oo-groupoids presented via topological
spaces, which has various problems.  This is particularly an issue in
cohesive type theory, where there is a separate "point-set level"
notion of path that it is important to distinguish from
identifications.

On Mon, May 4, 2020 at 7:48 AM Stefan Monnier <mon...@iro.umontreal.ca> wrote:
>
> > I don't think using "identification" necessarily implies any
> > difference between "identification" and "equality".  I don't think of
> > it that way.  For me the point is just to have a word that refers to
> > an *element* of an identity type.  Calling it "an equality" can have
> > the wrong connotation because classically, an equality is just a
> > proposition (or a true proposition), whereas an element of an identity
> > type carries information.  Calling it "an identification" suggests
> > exactly the information that it carries: a way of identifying two
> > things.
>
> I thought that's what "path" was for?
>
>
>         Stefan "who really doesn't know what he's talking about"
>