Iris je opravdu velmi cool (i když pro mě je to pořád matoucí, protože logiku vůbec neznám a poprvé jsem se s ní setkal přímo přes HoTT, takže náhlé ztracení závislých typů je překvapivé a trochu neohrabané).