Iris on todella, todella siisti (vaikka se on minulle edelleen hämmentävää, koska en tunne logiikkaa lainkaan ja ensimmäinen kosketukseni siihen oli kirjaimellisesti HoTT:n kautta, joten riippuvaisten tyyppien yhtäkkiä menettäminen on yllättävää ja vähän kömpelöä).