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?
 A: The HoTT book makes a difference between axioms and rules in the "Open problem" section of its Introduction chapter. See also the "Basic metatheory" chapter in Appendix A.4.
This is related to the constructivity property of the theory, and more accurately to its canonicity property. In short, we could say that an axiom is a rule of inference that is not constructive.
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$.
This good property holds when you restrict HoTT to the inductive types defined using the uniform pattern consisting in the formation / introduction / elimination and computation rules.
In the HoTT book, the canonicity property is lost when you add other inference rules that do not match that pattern, such as the axiom of choice, the law of excluded middle, function extensionality, or univalence. A term defined with such axioms cannot be reduced by normalization to a canonical form defined with only the constructors: the axioms "do not compute", they postulate the existence of a canonical term with an expected property, but do not tell you how to effectively compute this canonical term.
