Homotopy Type Theory Learning Seminar

Winter and Spring 2016

Essential information

Organized by: Dan Christensen and Chris Kapulkin.
Time: Tuesdays 1:30 - 3:00 PM.
Location: MC 107.

Topics

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 n-Types (part 1)

Following Chapter 7 of the HoTT Book, I will present some basic properties of Homotopy n-Types.
February 2nd Mitchell Riley Homotopy n-Types (part 2)

Following Chapter 3 of the HoTT Book, I will present some properties of (-1)- and 0-types; 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 type-theoretic 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 W-types 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 0-truncations, 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 non-trivial 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.