@mortberg @ecavallo For ordinary equivalences, there is no map Equiv(A, B) → Id(A,B) for all A, B. An explicit description of ordinary equivalences is in Remark 4.13. Types are given by pairs (A : U) × U^A. In the empty context, ordinary equivalences are essentially ordinary equivalences on the first comment but only dependent logical equivalences (i.e. maps back and forth) between the second ones. So the types (1, λ_. 1) and (1, λ_. 2) are equivalent but not equal (types like these are also used to refute funext, see Definition 5.1).