HoTT/book — pull request #641 by mikeshulman (2014-03-02 22:51:14+00:00)
Title: IoI is transport

Did we really not ever mention explicitly that these are the same?