### Article

## Model structures on categories of models of type theories

Models of dependent type theories are contextual categories with some additional structure. We prove that if a theory T has enough structure, then the category T-Mod of its models carries the structure of a model category. We also show that if T has Σ-types, then weak equivalences can be characterized in terms of homotopy categories of models.

Kant famously argued that elementary geometrical statements such as Euclid's Triangle Angle Sum theorem cannot be deduced from the rst principles by purely logical means because their proofs require extra-logical geometrical constructions [1, A719/B747]. The discovery of non-Euclidean geometries in the 19-th century made Kant's analysis of geometrical reasoning untenable in its original form, and throughout the following 20-th century it was generally viewed as fundamentally mistaken or at least wholly outdated. However the recently emerged Homotopy Type theory (HoTT) and the related program of building new \univalent" foundations of mathematics provide a formal and conceptual basis for revising, once again, the epistemic role and logical function of extra-logical constructions in mathematical (and other) proofs [2].

The received notion of axiomatic method stemming from Hilbert is not fully adequate to the recent successful practice of axiomatizing mathematical theories. The axiomatic architecture of Homotopy type theory (HoTT) does not ft the pattern of formal axiomatic theory in the standard sense of the word. However this theory falls under a more general and in some respects more traditional notion of axiomatic theory, which I call after Hilbert and Bernays constructive and demonstrate using the Classical example of the First Book of Euclid’s Elements. I also argue that HoTT is not unique in the respect but represents a wider trend in today’s mathematics, which also includes Topos theory and some other developments. On the basis of these modern and ancient examples I claim that the received semantic oriented formal axiomatic method defended recently by Hintikka is not self-sustained but requires a support of constructive method.

Finally, I provide an epistemological argument showing that the constructive axi omatic method is more apt to present scientifc theories than the received axiomatic method.

The identity concept developed in the Homotopy Type theory (HoTT) supports an analysis of Frege's famous Venus example, which explains how empirical evidences justify judgements about identities. In the context of this analysis we consider the traditional distinction between the extension and the intension of concepts as it appears in HoTT, discuss an ontological signicance of this distinction and, nally, provide a homotopical reconstruction of a basic kinematic scheme, which is used in the Classical Mechanics, and discuss its relevance in the Quantum Mechanics.

We consider certain spaces of functions on the circle, which naturally appear in harmonic analysis, and superposition operators on these spaces. We study the following question: which functions have the property that each their superposition with a homeomorphism of the circle belongs to a given space? We also study the multidimensional case.

We consider the spaces of functions on the m-dimensional torus, whose Fourier transform is p -summable. We obtain estimates for the norms of the exponential functions deformed by a C1 -smooth phase. The results generalize to the multidimensional case the one-dimensional results obtained by the author earlier in “Quantitative estimates in the Beurling—Helson theorem”, Sbornik: Mathematics, 201:12 (2010), 1811 – 1836.

We consider the spaces of function on the circle whose Fourier transform is p-summable. We obtain estimates for the norms of exponential functions deformed by a C1 -smooth phase.

This proceedings publication is a compilation of selected contributions from the “Third International Conference on the Dynamics of Information Systems” which took place at the University of Florida, Gainesville, February 16–18, 2011. The purpose of this conference was to bring together scientists and engineers from industry, government, and academia in order to exchange new discoveries and results in a broad range of topics relevant to the theory and practice of dynamics of information systems. Dynamics of Information Systems: Mathematical Foundation presents state-of-the art research and is intended for graduate students and researchers interested in some of the most recent discoveries in information theory and dynamical systems. Scientists in other disciplines may also benefit from the applications of new developments to their own area of study.