Iris 非常非常酷（雖然對我來說仍然有點困惑，因為我根本不懂邏輯，而我第一次接觸它實際上是通過 HoTT，所以突然失去依賴類型讓我感到驚訝且有點笨拙）。