Isomorphic Structures of any Kind are `Equal' in HoTT: But What... Structure? - Peter Aczel