Midwest Homotopy Type Theory Seminar
- Dates: May 26-27, 2018
- Place: University of Western Ontario, London (Canada)
- Organizer: Chris Kapulkin (kkapulki at uwo.ca)
All talks will take place in Middlesex College, room 107. Coffee and lunch will be served in room 108.
||Carlo Angiuli (Carnegie Mellon)
||Dan Christensen (Western)
||Luis Scoccola (Western)
||Robert Rose (Indiana)
||End of the meeting!
||Paige North (Ohio State)
||Simon Cho (Michigan)
- Carlo Angiuli (Carnegie Mellon), Cartesian cubical type theory
This talk will present Cartesian cubical type theory, an extension of homotopy type theory with a constructive semantics in which types are cubical sets of computer programs equipped with uniform Kan operations. Unlike homotopy type theory, Cartesian cubical type theory enjoys the canonicity property: every closed term of boolean type evaluates to true or false. I'll explain why canonicity holds and why it's important, show examples of proofs from HoTT that become much simpler in this system, and compare and contrast this system with the cubical type theory of Cohen et al.
- Simon Cho (Michigan), Weak equivalences between models of type theory (jww Cory Knapp, Clive Newstead, and Liang Ze Wong)
We recall notions of models of type theory, each exhibiting a different degree of strictness/stability of structure, and follow the program laid out by Kapulkin-Lumsdaine towards establishing the conjecture that all of these models are homotopically equivalent in some appropriate sense. Each category of models of type theory supports a notion of weak equivalence, stemming from identity type structure. Furthermore, previous work (by e.g. Kapulkin-Lumsdaine and Lumsdaine-Warren) give comparison functors between these categories of models. Using the work of Kapulkin-Lumsdaine as a template, we define weak equivalences between these categories themselves; the comparison functors then exhibit weak equivalences of categories-with-weak-equivalences. With guidance from Chris Kapulkin and Emily Riehl.
- J. Daniel Christensen (Western), Localization in homotopy type theory
This talk will present results about localization at a prime in homotopy type theory. The main result is that for a pointed, simply connected type X, the natural map from X to its p-localization induces algebraic localizations on all homotopy groups. In order to prove this, I'll describe new results about general reflective subuniverses and their separated types, including the fact that the separated types form a reflective subuniverse. As key steps towards proving the main theorem, I'll explain how localization at a prime commutes with taking loop spaces for a pointed, simply connected type, and explicitly describe the localization of an Eilenberg-Mac Lane space K(G,n) with G abelian.
- Paige North (Ohio State), A directed homotopy type theory
In this talk, I will propose a directed type theory. The goal of this project is to develop a type theory which can be used to describe directed homotopy theory and category theory. At the core of this type theory is a `homomorphism’ type former whose terms are meant to represent homomorphisms or directed paths. Its rules are roughly analogous to those of Martin-Löf’s identity type. There is an interpretation into the category of small categories. I will sketch this interpretation and the homotopy theory that it describes.
- Robert Rose (Indiana), On the natural numbers in elementary (∞,1)-toposes
While the existence of a natural numbers object is independent of the axioms of a 1-topos, Shulman's proposed definition of an elementary (∞,1)-topos allows several promising candidates to be constructed. One such is the loop space of the circle, which intuition suggests might even be taken to be the definition of the integers if its structure were discernible without independently constructed W-types. We have conjectured that an NNO (and hence other W-types) may indeed be obtained from the loop space of the circle. In this talk, I will present our progress on this conjecture.
- Luis Scoccola (Western), Congruence closure in intensional type theory
The main purpose of congruence closure algorithms is to automate the application of basic properties of equality, such as transitivity and congruence (i.e. x = y implies f(x) = f(y)). We describe an approach for a congruence closure algorithm for intentional type theory that is compatible with Univalence, takes care of some coherence problems, and is still useful when doing set-level mathematics. A proof of concept implementation is being done using the metaprogramming framework of Lean 3. Both the algorithm and its implementation are work in progress.
There is no registration fee and no formal registration procedure. Those planning to attend should contact Chris Kapulkin (kkapulki at uwo.ca) to help plan the event, e.g., make sure that we have food for everyone.
Detailed information about parking on Western's campus can be found here.
The Medway Lot (Lot R) is open to visitors and free of charge on weekends. Distance to Middlesex College: 700 meters.
The Middlesex Lot (Lot G) is open to visitors on weekends at a flat rate of C$7 per day. Distance to Middlesex College: 10 meters.
Participants should arrange their own accommodation. We have negotiated preferred rates at the following hotels from May 25-28:
- DoubleTree by Hilton. King size rooms (sleep 1-2 people) at the rate C$135 + tax per night (approx. $105). Booking code: MHT under "Group code", expired on April 30.
- Ontario Residence Hall. Two-bedroom suites with a shared bathroom, at the rate C$144-154 per suite or C$72-77 (approx. $57-61) per room. Booking code: please indicate "Midwest HoTT" in the "Group Name" field on the website. If two people want to share the same bedroom or suite, they should indicate it in the "Comments" section. The payment will be upfront on the day of arrival.
We acknowledge the support of the School of Mathematical and Statistical Sciences at the University of Western Ontario.