See:

  • Jonathan Sterling, Carlo Angiuli, and Daniel Gratzer. “A Cubical Language for Bishop Sets”. In: Logical Methods in Computer Science 18.1 (Mar. 2022). doi: 10.46298/lmcs-18(1:43)2022. - Section 1 for a brief history of equality in type theory

Corrections (version of March 2026):

Submitted:

  • p.2: "Given that determining the result of a program is in general undecidable" - insert "the problem of" before "determining"
  • p.4: "vector has length at least one" - insert "of" before "at least one"
  • p.7: "we can now define not only variadic functions but even higher-order functions taking variadic functions as input, such as apply which applies" - maybe add commas: "functions, but"; "apply, which"
  • p.13: "closed vector" - what is it?
  • p.17: "ignoring the rules marked with (ITT), which are present only in intensional type theory" - change "ignoring" to "ignore"
  • p.17: "These questions lead to..." - change "questions" to "topics"
  • /p.21: some rules are referenced not by content ("rules for") but by name ("lambda rule", "variable rule"), but displayed rules are not named/
  • p.22: "their thoughts" - should be "the thoughts"?
  • p.23: "are η-equivalences" - insert "called" after "are"
  • p.23: function "FreeVariables" is referenced but not defined
  • p.24: "“junk” judgments that should not correspond to elements of some Tm(Γ, A)" - change "some" to "any" or rephrase
  • p.25: "η-rule of functions" - change "of" to "for"?
  • p.25: "we will notice ... in the right-hand side of the η-rule of functions, f is in context Γ, x : A, whereas in the premise and left-hand side it is in Γ" - I fail to notice this in the rule as it is given in the text ;)
  • p.27: "arbitrary terms of arbitrary type to occur within types" - change "type" to "types"
  • p.27: "rules of all ... to all depend on one another" - is double-"all" intentional?
  • p.35: "construct a substitution that we will name γ .A, satisfying" - change "that" to "which" and insert a comma before it
  • p.36: "There continue to be a few notational shifts" - this sounds wrong ;)
  • p.67: "These rules quickly become tedious, so we write only their introduction" - change "These" to "The" or "their" to "the"
  • p.78: "is “propositions as some types” too restrictive, or it is genuinely incorrect" - change "it is" to "is it"
  • p.84: "proposition that maps out into only other propositions" - change "into only" to "only into"
  • p.84: "Where are the β and η principles?" - change "principles" to "rules"

Also submitted:

  • p.94: "we will need to wonder whether this existence is unique" - rephrase "existence is unique"
  • p.96: "closed derivation trees" - defined where?
  • p.102: "synthesizing (lam e0)" - insert "the type of" after "synthesizing"
  • p.109: "canonicity models" - change to "models establishing canonicity"?
  • p.133: "Its rules are collected in Appendix A, ignoring the rules marked with (ETT) which are present only in extensional type theory." - change "ignoring" to "; ignore" here as on p.17
  • p.144: "initial letter of pre-existing mathematical terminology" - change "terminology" to "term"
  • p.149: "closed proof" - what is it? (same on p.338)
  • p.153: "We leave the remaining structure as an exercise." - rephrase "remaining structure"?
  • p.181: "As in Section 2.5 we will define" - add comma after "2.5"
  • p.189: "extension of ITT by an simple axiom" - change "an" to "a"
  • p.189: "closed elements" - defined where?
  • p.189: "give it a new mapping in property which gives" - add comma before "which"; change "mapping in" to "mapping-in"
  • p.190: "present the additional operations necessary to manipulate them" - drop "the"; who is "them"?
  • p.190: "though still not in the entirety" - change "the" to "their"
  • p.190: "working knowledge of cubical type theory, rather than" - drop the comma
  • p.190: "we internalized all the rules of the identity type came more-or-less for free" - drop "came"
  • p.192: "Before when identity types internalized definitional equality" - add comma after "before"
  • p.199: "closed types" - defined where? "type constructor is closed" - same
  • p.206: "As with any other type we must" - add comma before "we"?
  • p.206: "this sketch omits a great many details" - drop the "a"?
  • p.219: "our focus throughout this book has been on syntactic models of type theory. In this chapter, we systematically consider models of type theory" - contrasted notions "syntactic models" and "systematic consideration of models" are orthogonal
  • p.274: "This is mismatch of equality versus coherent isomorphism is commonly referred to" - drop the first "is"