On Feb 25, 2017, at 2:19 PM, Thierry Coquand <Thierry...@cse.gu.se> wrote: “Bishop set” which correspondsto the fact that any two paths between the same end points are -judgmentally- equal.