Is there a distinction between rules of inference and axioms in Homotopy Type Theory (HoTT)?

I'm taking rules of inference to be metalinguistic and to describe when you can write down a certain syntactic expression in the object-language given that you already have others written down (e.g. &-Intro in Natural Deduction). I'm taking an axiom to be a syntactic expression in the object-language (logical or non-logical, if the distinction matters, please mention that).

I have been told there is no distinction between rules of inference and axioms in HoTT. Being charitable (I don't think this is a denial in a distinction of the concepts, just their extensions), I am taking this to mean every rule of inference is an axiom and vice-versa.

This is not obvious to see from glancing at the book Homotopy Type Theory: Univalent Foundations of Mathematics. For example, page 434 has the $$\Pi$$-FORM rule which seems clearly like an inference rule in the metalanguage as it features a turnstile which I take it is not part of the object-language (and also the notation which utilizes the horizontal bar). If there is no distinction, then somehow this should be formalizable simply as a single expression in the object-language? And the same for any other rule?

An example I was given to demonstrate this was the rule:

if $$\Gamma\vdash a:A$$ and $$\Gamma\vdash b:B$$, then $$\Gamma\vdash (a,b):A\times B$$. And, the type $$A\rightarrow B\rightarrow A\times B$$.

To me this seems like conflating rules of inference with types just because there is a correspondence between the two.

So is there a distinction between rules of inference and axioms in HoTT?

• Who says there is no distinction between rules and axioms in HoTT? Mar 24 at 4:31
• I'll try to answer your question in a longer post, but I'll just quickly point out here that the expression you wrote toward the end requires a small correction. It should presumably read "if $\Gamma \vdash a : A$ and $\Gamma \vdash b : B$, then $\Gamma \vdash (a, b) : A \times B$." Mar 24 at 5:41
• In my opinion, you are conflating two different distinction here: the distinction between the object language and the metalanguage, and the orthogonal distinction between axioms and rules of inference. An axiom, to me, is simply a rule of inference with no premises. Mar 24 at 13:09
• @Pilcrow I know of this way of viewing them and it might be an adequate way to conceptualize rules of inference and axioms, but I don't know how standard this is in the logic community. For example, this doesn't align well with the phrase "axioms of ZFC" and the like. People don't think about axioms of ZFC as "rules of inference for set theory with no premises". They just take them to be expressions in the object language that are taken to be the starting point for the theory. Mar 24 at 15:18
• As best as I can tell, without having heard exactly what you've been told, I would say that what you've been told is wrong. HoTT maintains a distinction between rules of inference and axioms just like most other type theories, as you've explained. Can you give a citation or reference to whoever told you this? Mar 27 at 1:05

In a perfectly constructive setting, you expect that any closed term $$a$$ of type $$A$$ reduces by normalization to a canonical form that is a composition of the constructors of $$A$$.