从 Induction 到 Axiom K, UIP, J-rules
前阵子正看着 HoTT Book 中 1.12 节,即讲述 identity type 与 path induction 之类的概念,透过 Agda 对其研究与学习之后决定写一篇文章记录下有关这些概念的一些理解,以巩固一下自己对这些概念的认识。
引言
在 Agda 中,我们或多或少在一些需要证明命题等价性的 module 中可能会看到 {-# OPTIONS --without-K #-} ...
続きを読む…