In a Hilbert-style non-logical axiomatic theory the semantics of logical symbols is rigidly fixed, while the interpretation of non-logical symbols usually varies giving rise to different models of the given theory. All non-logical content of such a theory is comprised in its non-logical axioms (e.g., axioms of ZF) while rules, which generate from these axioms new theorems, belong to the logical part of the theory (aka underlying logic). An alternative approach to axiomatization due to Gentzen amounts to a presentation of formal calculi in the form of systems of rules without axioms. Gentzen did not try to extend his approach to non-logical theories by considering specific non-logical rules as a replacement for non-logical axioms. However the more recent work in Univalent Foundations of Mathematics  suggests that the Gentzen-style rule-based approach to formal presentation of theories may have important applications also outside the pure logic. Areasonwhy onemay prefer a rule-based formal representation is that it ismore computerfriendly. This, in particular, motivates the recent work on the constructive justification of the Univalence Axiom via the introduction of new operations on types and contexts . However this pragmatic argument does not meet the related epistemological worries. What kind of knowledge may represent a theory having the form of a bare system of rules? Is such a formof a theory appropriate for representing a knowledge of objective human-independent reality? How exactly truth features in rule-based non-logical theories? Using HoTT as a motivating example I provide some answers to these questions and show that the Gentzen-style rule-based approach provides a viable alternative to the standard axiomatic approach not only in logic but also in science more generally.