Iris 非常非常酷（尽管对我来说仍然有些困惑，因为我根本不懂逻辑，而我第一次接触它实际上是通过 HoTT，所以突然失去依赖类型让我感到惊讶，并且有点笨拙）。