December 31st
Today I learned about equality types. This is along the lines of propositions as types, where if we want to "prove'' $a=b,$ we have to inhabit $a=b$ somehow. As expected, our main tool for constructing functions is induction, which is called path induction in order to allude to the coming homotopy type theory. Path induction states that for a family\[C:\prod_{(a,b:A)}(a=_Ab)\to\UU,\]and witnesses\[c:\prod_{a:A}C(a,a,\refl_a),\]then we have a function\[f:\prod_{(a,b:A)}\prod_{(p:a=_Ab)}C(a,b,p)\]satisfying $f(a,a,\refl_a)\equiv c(a).$ Here, $\refl_a$ refers to a "reflexive'' proof of the equality $a=a.$ Stated succinctly, we can write\[\op{ind}_{=A}:\left(\prod_{(a,b:A)}(a=_Ab)\to\UU\right)\to\left(\prod_{a:A}C(a,a,\refl_a)\right)\to\left(\prod_{(a,b:A)}\prod_{(p:a=_Ab)}C(a,b,p)\right)\]which satisfies $\op{ind}_{=A}(C,c)(a,a,\refl_a)\equiv c(a).$
As usual, path induction lets us construct dependent functions from equality types from the "canonical'' elements $\op{refl}_\bullet.$ This actually makes me somewhat uncomfortable, in that we're being told what to do with non-reflexive elements without being told, so we're getting a surprising amount of power. Homotopically, this is roughly defining a continuous functions over all paths after having only been told what to do with constant paths, which doesn't make much sense to me.
I guess I should mention based path induction. Essentially, we fix $a:A,$ in that we now take a family\[C:\prod_{x:A}(a=_Ax)\to\UU\]with witness\[c:C(a,\refl_a),\]and we get a function\[f:\prod_{(x:A)}\prod_{(p:a=_Ax)}C(a,p).\]The two forms of induction are equivalent (we can derive each from the other), but this is not easy to see.