Organized by: Dan Christensen and Chris Kapulkin.
Time: Tuesdays 1:30  3:00 PM.
Location: MC 107.
Date  Speaker  Title and abstract 

January 5th  Organizational meeting 

January 12th  Chris Kapulkin  Properties of the Identity Type (part 1) Following Chapter 2 of the HoTT Book, I will present the main properties of the Identity Type. 
January 19th  Chris Kapulkin  Properties of the Identity Type (part 2) Following Chapter 2 of the HoTT Book, I will continue presenting the main properties of the Identity Type. 
January 26th  Mitchell Riley  Homotopy nTypes (part 1) Following Chapter 7 of the HoTT Book, I will present some basic properties of Homotopy nTypes. 
February 2nd  Mitchell Riley  Homotopy nTypes (part 2) Following Chapter 3 of the HoTT Book, I will present some properties of (1) and 0types; propositions and sets. 
February 9th  Cihan Okay  Introduction to the Coq proof assistant This talk will be a basic interactive introduction to Coq. I will start with simple operations on natural numbers, then move on to functions on arbitrary types, and illustrate how to prove a logical statement in computer. 
February 16th  No talk!  Reading Week 
February 23rd  Marco Vergura  Equivalences and the Univalence Axiom (part 1) We introduce Voevodsky's Univalence Axiom and see some of its consequences in type theory. We also start studying various definition of typetheoretic equivalences. 
March 1st  Marco Vergura  Equivalences and the Univalence Axiom (part 2) Following Chapter 4 of the HoTT book, we continue our journey in the various characterizations of equivalences in Type Theory. We also show how Function Extensionality follows from the Univalence Axiom. 
March 8th  Karol Szumiło  Formalized Homotopy Theory (part 1) I will present formal proofs of selected results discussed in preceding seminar talks using the Coq library UniMath. 
March 15th  Karol Szumiło  Formalized Homotopy Theory (part 2) I will present formal proofs of selected results discussed in preceding seminar talks using the Coq library UniMath. 
March 22nd  Karol Szumiło  Formalized Homotopy Theory (part 3) I will present formal proofs of selected results discussed in preceding seminar talks using the Coq library UniMath. 
March 29th  James Richardson  Inductive types (part 1) In this talk we will introduce Wtypes and discuss several examples of inductive types. 
April 5th  James Richardson  Inductive types (part 2) In this talk we will discuss uniqueness results for inductive types, with particular focus on identity types. 
April 12th  Pál Zsámboki  Higher Inductive Types (part 1) We introduce the first example of a higher inductive type, S^1, for which we prove a universal property. Then after discussing the interval I, we move on to spheres. We finish with finite CW complexes. 
April 19th  Pál Zsámboki  Higher Inductive Types (part 2) We start by discussing pushouts and (1) and 0truncations, then we use these to discuss quotients of sets by mere relations and algebraic structures on sets. We finish with a particular case of the flattening lemma, which says that if W is a particular higher inductive type, then the total space of the fibration corresponding to a presheaf on W is equivalent to an appropriate higher inductive type. 
April 26th  No talk!  
May 3rd  Andrés Felipe Fontalvo Orozco  The Univalence Axiom and Higher Inductive Types in action Selected topics in chapter 8 of the HoTT book will be presented to illustrate how homotopy theory can be developed within type theory. 
May 25th  Christian Sattler  Algebraic model structures via "glueing" Consider a Grothendieck topos with a functorial cylinder with connections and a choice of generating cofibrations. Together, this induces a naive notion of fibration. We give sufficient coditions under which this gives rise to an (algebraic) model structure. The key point will be the glueing construction of Cohen et al., a recent combinatorial discovery that allows for constructively extending fibrations along trivial cofibrations without resorting to a theory of minimal fibrations. 
June 7th  Dan Christensen  Computation and data structures in Coq I will give an overview of how to do computations in Coq, including nontrivial recursive computations. I will also describe data structures such as lists and trees, and show how they can be manipulated. The corresponding Coq file. 
June 28th  Mitchell Riley  (2)Category Theory in HoTT In this talk I will describe the development of category theory within HoTT and what it means for a category to be univalent. 
July 5th  Jason Brennan  Impartial Game Theory in Coq I will provide a brief introduction to impartial game theory consisting of examples of games as well as elementary operations on them. This will be followed by a presentation of their syntactic counterparts in Coq, culminating in formal proofs of several basic theorems. 
For more information, contact Chris Kapulkin.
Last updated by Chris Kapulkin on June 27th, 2016.