HoTT-StudyGroup

Tübingen Study Group for Homotopy Type Theory

This repository is used for coordinating the Study Group on Homotopy Type Theory in Tübingen and to share articles, links, books, dates, etc...

##Doodle Poll

Insert your available time slots in the doodle poll: Doodle [We have now settled on the Monday Tuesday 14-16 timeslot.]

---

##Schedule The meetings will take place on Mondays Tuesdays at 14:1514:00 in room A302 C109 at the Sand. The preliminary schedule looks as follows:

• 13 Dec 2016 : Organisation of the Reading Group, Backgrounds in Type theory, Introduction to Martin-Löf dependent type theory and its identity types. (David + Ingo)

In the first meeting we discussed:

1. The two kinds of judgments of Martin-Löf type theory.
2. The FIEC-Schema for introducing new types (Formation, Introduction, Elimination, Computation Rules).
3. Nondependent Product and Sum Types.
4. Dependent Function Type (= Pi Type) and Dependent Product Type (= Sigma Type).
5. The Type of natural numbers.
6. The provability of the type-theoretic version of the Axiom of Choice.

• 20 Dec 2016 : We will discuss chapter 1 of the HoTT book, wrap up the remaining questions about the dependent function + product types and probably concentrate on the Identity-Type (propositional Identity) (Ingo)

We discussed:

1. The FIEC rules for the identity type.
2. How the Elimination principle for the identity type does not allow us to deduce the Uniqueness of Identity Proofs (UIP) property.
3. How to strengthen the identity type with Streicher's axiom K so that UIP is deducible.
4. The interpretation of the Identity Type as the Type of Paths in a topological space. (And the type of paths between these paths as the homotopies between the paths)
5. Two examples of Higher Inductive Types: The circle S1 and the Type of Natural numbers mod 2.

See also: Dan Licata on Identity Types

• 10 Jan 2017 : We will discuss from Chapter 2 the beginning until section 2.4 inclusive. (Philipp)

Groupoids and Puzzles Alan Weinstein on Groupoids (PDF)

• 17 Jan 2017:

• 24 Jan 2017: We dicuss Ladyman's alternative justification for path induction and the encode/decode pattern.

Identity in Homotopy Type Theory, Part I: The Justification of Path Induction

• 31 Jan 2017 : We discussed sections 2.12 to 2.14. This mainly involved the characterization of positive types using the code-decode-procedure.

• 07 Feb 2017 : We will discuss the beginning of Chapter 3 until section 3.4 inclusive. (Ingo)

  We discussed:

  1. The incompatibility of Univalence and LEM
  2. The trivial truth of AC in its "naive" form
  3. (Non-)Existence of relationships between isProp, isSet, Dec and DecEq.

• 14 Feb 2017 : We will discuss the second half of Chapter 3 (sections 3.5–3.11). (Philipp)

• 21 Feb 2017 : We will discuss the rest of Chapter 3, skip Chapter 4 and continue with Chapter 5 (until 5.3, W-Types)

  We discussed:

  1. Contractibility
  2. W-types

• 04 Apr 2017 : We will discuss sections 5.4 to 5.6.

  We discussed:

  1. Proof of isSet(Universe)
  2. Inductive types as initial algebras
  3. F-algebras in general Bartosz Milewski on F-Algebras

• 11 Apr 2017 : We will discuss the rest of Chapter 5, starting at 5.6. (Philipp)

  We discussed:

  1. Generalizations of Inductive Types (in particular inductive-inductive and inductive-recursive)
  2. "Free generation" of inductively defined types
  3. Exercises 5.1, 5.2 and 5.7

• 18 Apr 2017 : We will discuss the the beginning Chapter 6, Sections 6.1 until 6.3 (Ingo)

  Skipped

• 25 Apr 2017 : see 18 Apr

  We discussed: this.

• 2 Mar 2017 : We will discuss Sections 6.4 until 6.5 (David)

  We discussed: this.

• 9 Mar 2017 : We will discuss Sections 6.8 until 6.10 (Philipp)

  We discussed:

  1. categorical constructions in detail ((co-)equalizers, pullback, pushouts, etc)
  2. topological constructions (suspension, join, cofiber, wedge, smash product) as pushouts

• 16 Mar 2017 : We will discuss Sections 6.9 until 6.11

  We discussed:

  1. Truncations (shortly)
  2. Quotients (shortly)
  3. Algebras as HIT

• 30 Mar 2017 : Cubical Type Theory

  Possible sources:

  1. Angiuli, Harper, Wilson: Computational Higher-Dimensional Type Theory
  2. Clive Newstead: Cubical sets
  3. Cohen, Coquand, Huber, Mörtberg: Cubical Type Theory: a constructive interpretation of the univalence axiom

---

Links

• The official HoTT Book: HoTT Book
• Robert Harper's Video Lectures: Lectures
• nLab Article: nLab
• Wikipedia Article: Wikipedia
• Video List from the Fields Institute Workshop: Fields Institute
• A Meaning Explanation of HoTT: FOM Mailing List
• Lean Tutorial by Jeremy Avigad: Tutorial
• FOMUS talks on youtube: FOMUS 2016

---

Computer Implementations of HoTT

• Coq Library on Github: Github
• Agda Library on Github: Github
• Lean 0.2 Library on Github: Github