|
Die folgenden Informationen sind noch nicht freigegeben und deshalb unverbindlich: Homotopy Type Theory SemesterSoSe 2026 Lecturer Tashi Walde Type of course (Veranstaltungsart) Vorlesung German title Homotopietypentheorie Contents This course is an introduction to univalent mathematics and homotopy type theory. This is an alternative foundation of mathematics which differs from other foundations (such as first order logic + ZFC) in at least two ways: - Mathematical objects (e.g. sets) and statements about them (propositions) exist in the same logical framework rather than being in two distinct layers: this means that conceptually there is no longer a distinction between providing a proof and performing a construction. - Equality between two objects is no longer a property, but structure. For example, two object can be equal in multiple ways, and it makes sense to ask whether those equalities are equal in turn. ----- Voevodsky's univalence axiom asserts that there is no difference between equality and equivalence. For example, this lets us correctly treat isomorphic groups as equal with all logical benefits derived from this; something that would be unthinkable in set-theoretic foundations. Homotopy Type Theory is constructive by default. But if required, it can easily be extended with classical non-constructive axioms such as the law of the excluded middle or the axiom of choice. Literature - The HoTT Book (https://homotopytypetheory.org/book/) - Introduction to Univalent Foundations of Mathematics with Agda (Escardó) - Introduction to Homotopy Type Theory (Rijke) Recommended previous knowledge Prerequisites: you know what an isomorphism is (e.g. of sets, vector spaces or groups). Some previous exposure to category theory and/or (algebraic) topology will be very helpful, but is not required. Time/Date Mo 14--16, Mi 12--14, Fr 10--12 (4 hours lecture, 2 hours exercises) Course homepage GRIPS (Disclaimer: Dieser Link wurde automatisch erzeugt und ist evtl. extern) Registration
BV, MV, MGAGeo ECTS 9 ECTS |