Details.
HTT Seminar Spring 2019
4:00 - 5:00 Wednesdays, Linde Hall 187
Contact: panagio at caltech.edu

The plan currently is to go over the first 4 chapters of HoTT book and extract some condensed notes. Email me if you want to volunteer for any of the following weeks for which we do not already have a speaker:

Calendar/Speakers/Notes.

• (April 17) Forte Shinko will introduce us to Type Theory. Forte's Notes Relevant reading: sections 1.1-1.12 of HoTT.


• (April 24) Forte Shinko will introduce us to Type Theory (part 2).Forte's Notes Relevant reading: sections 1.1-1.12 of HoTT.


• (May 1) Tamir Hemo will cover Sections 2.1-2.4: Types are higher groupoids, functions are functors, type families are fibrations, homotopies and equivalences.


• (May 8) Justin Campbell will cover Sections 2.5-2.15: The higher groupoid structure of type formers, cartesian product types, Σ-types, the unit type, Π-types and function extensionality, universes and the univalence axiom, identity type, coproducts, natural numbers, example: equality of structures, universal properties.


• (May 15) Aristotelis Panagiotopoulos will cover Sections 3.1-3.11. Sets and n-types, propositions as types, mere propositions, classical vs intuitionistic logic, subsets and propositional resizing, the logic of mere propositions, propositional truncation, the axiom of choice, the principle of unique choice, when are propositions truncated?, contractibility.


• (May 22) Sasha Yom Din will cover Sections 4.1-4.5. Notes. Quasi-inverses, half adjoint equivalences, bi-invertible maps, contractible fibers, on the definition of equivalences.


• (May 29) CANCELLED Sections 4.6-4.9. Closure property of equivalences, the object classifier, univalence implies function extensionality.


• (June 5) Open to suggestions. A suggestion for the last three seminars is to work our way to the computation of π_1(S) via HoTT


• (June 12) Open to suggestions. A suggestion for the last three seminars is to work our way to the computation of π_1(S) via HoTT


• (June 17) Open to suggestions. A suggestion for the last three seminars is to work our way to the computation of π_1(S) via HoTT

Home. Back to my website.