Categorical Logic (Shulman, 2016)
Related
Quotes:
Note that together our four principles say that insofar as possible, the “algebraic operations” in a categorical structure (such as composition and identities in a category or multicategory, permutation of domains in a symmetric multicategory, and so on) are exactly what we do not include as primitive rules in type theory! To put this differently, recall from the end of §1.2.2 that the initiality theorems for type theory are about showing that two different categories have the same initial object; we might then say that the effect of the above principles is to ensure that these two categories are as different as possible. This may seem strange, but to paraphrase John Baez, a proof that two things are the same is more interesting (and more useful) the more different the two things appear to begin with.
Tags: Type theory
#paper