20.500.12556/RUL-188192 Hopfovo vlaknenje v homotopski teoriji tipov delo diplomskega seminarja The Hopf fibration in homotopy type theory V delu obravnavamo Hopfovo vlaknenje v homotopski teoriji tipov. Predstavimo sintetično interpretacijo tipov kot prostorov in identifikacij kot poti ter razvijemo pojme transporta, homotopije, ekvivalence, povezanosti in homotopskih grup. Z višjimi induktivnimi tipi definiramo krog, suspenzije, sfere, potiske in spoje. S pomočjo $H$-strukture kroga in univalenčnega aksioma konstruiramo družino tipov nad sfero $\mathbb{S}^2$, katere izbrano vlakno je $\mathbb{S}^1$. Z lemo o sploščevanju pokažemo, da je njegov totalni prostor ekvivalenten sferi $\mathbb{S}^3$, in tako dobimo Hopfovo vlaknenje $$\mathbb{S}^1 \longrightarrow \mathbb{S}^3 \longrightarrow \mathbb{S}^2.$$ Izračunamo fundamentalno grupo kroga in pokažemo, da velja $\pi_1(\mathbb{S}^1)\simeq\mathbb{Z}$, njegove višje homotopske grupe pa so trivialne. Z uporabo dolgega eksaktnega zaporedja Hopfovega vlaknenja nato izpeljemo $$\pi_2(\mathbb{S}^2)\simeq\mathbb Z$$ ter $\pi_n(\mathbb{S}^2)\simeq\pi_n(\mathbb{S}^3)$ za vsak $n\geq 3$. In this thesis, we study the Hopf fibration in homotopy type theory. We present the synthetic interpretation of types as spaces and identifications as paths, and develop the notions of transport, homotopy, equivalence, connectedness, and homotopy groups. Using higher inductive types, we define the circle, suspensions, spheres, pushouts, and joins. With the help of the $H$-structure on the circle and the univalence axiom, we construct a type family over the sphere $\mathbb{S}^2$ whose distinguished fibre is $\mathbb{S}^1$. Using the flattening lemma, we show that its total space is equivalent to the sphere $\mathbb{S}^3$, thus obtaining the Hopf fibration $$\mathbb{S}^1 \longrightarrow \mathbb{S}^3 \longrightarrow \mathbb{S}^2.$$ We compute the fundamental group of the circle and show that $\pi_1(\mathbb{S}^1)\simeq\mathbb{Z}$, while its higher homotopy groups are trivial. Using the long exact sequence of the Hopf fibration, we then derive $$\pi_2(\mathbb{S}^2)\simeq\mathbb Z$$ and $\pi_n(\mathbb{S}^2)\simeq\pi_n(\mathbb{S}^3)$ for every $n\geq 3$. homotopska teorija tipov Hopfovo vlaknenje višji induktivni tipi univalenčni aksiom homotopske grupe sfere homotopy type theory Hopf fibration higher inductive types univa- lence axiom homotopy groups spheres true false false Slovenski jezik Angleški jezik Delo diplomskega seminarja/zaključno seminarsko delo/naloga 2026-09-19 08:15:27 2026-09-19 08:15:30 2026-09-21 16:50:56 0000-00-00 00:00:00 2026 0 0 0000-00-00 NiDoloceno NiDoloceno NiDoloceno 0000-00-00 0000-00-00 0000-00-00 515.1:510.6 164613 291892739 24126.pdf 24126.pdf 1 12BEAC7841A81C74450A979C1793A792 441185c1c7311e848e68b5d622312725bed88234a6ef8ed880276028b1979640 7715adbe-b3f1-11f1-8bc5-0050569b8976 https://repozitorij.uni-lj.si/Dokument.php?lang=slv&id=248221 Fakulteta za matematiko in fiziko 0 0 0