A Iris é muito, muito fixe (embora ainda confusa para mim, pois não sei lógica de todo e a minha primeira exposição a isso foi literalmente através do HoTT, então perder tipos dependentes de repente é surpreendente e meio desajeitado).