What are 2-morphisms in the category of proofs?

Question

After reading through "Categories for the practicing physicist" I came to learn there is a category whose objects are propositions $A,B,...$ and whose morphisms are proofs $f:A\rightarrow{B}$ that conclude from $A$ that $B$ holds. I would like to know what the 2-morphisms of this category correspond to.

Answer 1

Disclaimer: The following is informal, but hopefully morally correct. If not, I'm happy to be corrected.

When you build a syntactic $k$-category from a logical system, you will often need to do some identification on the level of $k$-morphisms based on the existence of witnesses of 'equivalence' of $k$-morphisms that are not part of the syntactical system itself. You can then step a level higher by making these witnesses the $k+1$-morphisms in the next higher syntactic category, again up to some notion of equivalence, and so on. In the limit, you reach homotopy type theory, where all identifications of terms come from the system itself in the form of other terms of the corresponding equality type.

Consider the bottom of this hierarchy, for example: Given a fixed set of propositional variables, you may form the initial Heyting algebra (i.e. small, skeletal, bicartesian closed $0$-category) over it by taking as objects the equivalence classes of intuitionistic propositional formulae, and by taking implication as the order relation. However, the objects witnessing the identification of two propositions, i.e. the actual proofs of their equivalence, are nowhere to be found in this construction.

This is fixed in the syntactic $1$-category attached to the system: Now you have honest propositional formulae, without any identification, as objects, and equivalence classes of proofs (in the form of $\lambda$-terms) as objects. Again, however, the equivalence of proofs is not defined through the system itself, but through the new notions of $\alpha/\beta$-conversion and rewrite rules for the various type formers. Interestingly, the fact that this $\lambda$-calculus is strongly normalizing gives rise to a decision procedure for intuitionistic propositional logic, while the decidability of equivalence of $\lambda$-terms themselves up to conversion and rewrite rules is again a difficult problem (I don't know if it's solved, I only found http://www.cs.nott.ac.uk/~txa/publ/lics01.pdf where this is proved for $\lambda$-calculus without a bottom type).

As a next step, Seely has introduced in http://www.math.mcgill.ca/rags/WkAdj/LICS.pdf a $2$-category where these conversion and rewrite rules are the $2$-morphisms, but I hadn't have time so far to look at it closely.

Anyway, I hope that the above is of some help, albeit imprecise.