Iris дуже-дуже класна (хоча для мене це все ще заплутано, бо я взагалі не знаю логіки, а мій перший досвід був буквально через HoTT, тож раптова втрата залежних типів дивує і трохи незграбна).