**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.