O nekontraktibilnosti krožnice v homotopski teoriji tipov

V članku so predstavljeni osnovni gradniki homotopske teorije tipov. Znotraj teorije je nato izpeljan preprost dokaz znanega dejstva iz algebraične topologije, da krožnica \(S^1\) ni kontraktibilna. Dokaz temelji na konceptu vlaknenja, ki je v homotopski teoriji tipov zelo osnovna konstrukcija. Namen članka je predstaviti uporabnost homotopske teorije tipov skozi primer dokaza, ki je klasično precej netrivialen, saj delo s homotopijami hitro zahteva veliko znanja iz topologije. Ker so poti popolnoma osnovni objekti v homotopski teoriji tipov, za razumevanje članka ni potrebno predznanje iz drugih matematičnih področij, seveda pa lahko pripomore k intuiciji pri nekaterih dokazih.

On the noncontractibility of the circle in homotopy type theory

The article presents the basic building blocks of homotopy type theory. Within the theory, a simple proof is then derived of the well-known fact from algebraic topology that the circle \(S^1\) is not contractible. The proof is based on the concept of a fibration, which is a very basic construction in homotopy type theory. The aim of the article is to present the usefulness of homotopy type theory through an example of a proof that is classically quite nontrivial, since working with homotopies quickly requires a great deal of knowledge of topology. Since paths are completely basic objects in homotopy type theory, no prior knowledge of other areas of mathematics is required to understand the article, although such knowledge can of course contribute to intuition in some of the proofs.