Types @Mim2022 @Rijk2022 Agda bibliography Category Theory HoTT Introduction into Everything lambda-calculus Logic natural-deduction Types