Midwest Homotopy Type Theory Seminar
Essential information
 Dates: May 2627, 2018
 Place: University of Western Ontario, London (Canada)
 Organizer: Chris Kapulkin (kkapulki at uwo.ca)
Schedule
All talks will take place in Middlesex College, room 107. Coffee and lunch will be served in room 108.
Time 
Saturday 
Sunday 
9 
Coffee 
Coffee 
9:30 
Carlo Angiuli (Carnegie Mellon) 
Dan Christensen (Western) 
10:30 
Coffee break 
Coffee break 
11 
Luis Scoccola (Western) 
Robert Rose (Indiana) 
12 
Lunch 
End of the meeting! 
2 
Paige North (Ohio State) 

3 
Coffee break 

3:30 
Simon Cho (Michigan) 

If you are planning to arrive on Friday, you may want to consider joining the locals for some social activities in the evening, including dinner and drinks. Please let Chris Kapulkin know that you are interested.
Talks
 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 KapulkinLumsdaine 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. KapulkinLumsdaine and LumsdaineWarren) give comparison functors between these categories of models. Using the work of KapulkinLumsdaine as a template, we define weak equivalences between these categories themselves; the comparison functors then exhibit weak equivalences of categorieswithweakequivalences. 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 plocalization 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 EilenbergMac 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 MartinLö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 1topos, 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 Wtypes. We have conjectured that an NNO (and hence other Wtypes) 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 setlevel 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.
Registration
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.
Parking
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.
Lodging
Participants should arrange their own accommodation. We have negotiated preferred rates at the following hotels from May 2528:
 DoubleTree by Hilton. King size rooms (sleep 12 people) at the rate C$135 + tax per night (approx. $105). Booking code: MHT under "Group code", expired on April 30.
 Ontario Residence Hall. Twobedroom suites with a shared bathroom, at the rate C$144154 per suite or C$7277 (approx. $5761) 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.
Sponsors
We acknowledge the support of the School of Mathematical and Statistical Sciences at the University of Western Ontario.