Frédéric Blanqui Anthony Bordg for the alignment of the types sum, list, option Amal Makni for the alignment of subtypes, quotient types and part of the type of real numbers