HoTT for Cools

1 Preface

Homotopy Type Theory is an exciting and relatively new area of mathematics. The main resource for learning it is a Free/Open Source book with the same name: Homotopy Type Theory: Univalent Foundations of Mathematics. I’m currently reading it and I decided to publish notes that I’m taking from it. For each chapter of the original book we have a corresponding chapter with the same name containing a cheat sheet of theorems of that chapter and some extra notes.

1.1 Disclaimer

- I am not a mathematician

- I am not a native English speaker

So be prepared for lots of mathematical or grammatical mistakes. However, this is a free book, so you can help me make it better. See the How to Contribute section.

- This book is a work in progress and will change frequently:

So always check that you have the latest release.

1.2 How to Contribute

This is a libre/open source project. It is hosted on GitLab and any contribution is welcomed and highly appreciated.

[TODO] Add detailed information on how to commit to a git repository for beginners.

1.2.1 List of Contributors

1.3 Acknowledgment

This book and most of its latex macros is based on the Homotopy Type Theory: Univalent Foundations of Mathematics book.

The PDF, web pages and e-books are produced with scripts around pandoc and other free software. see the GitLab page.

1.4 License

Except As Otherwise Noted, This Work Is Licensed Under A Creative Commons Attribution-ShareAlike 4.0 International License. To View A Copy Of This License, Visit: https://creativecommons.org/licenses/by-sa/4.0/

Code Samples Are Licensed Under The GNU General Public License v3.0. To View A Copy Of This License, Visit: https://www.gnu.org/licenses/gpl-3.0.en.html

2 Introduction

“Tell readers that Introduction is not essential for book understanding”1

The introduction gives a bird’s-eye overview of Homotopy type theory and its relation to other fields of mathematics. Unfortunately it intimidates newcomers and they might think that they won’t be able to understand the rest of the book. The good news is that the book is almost self sufficient. Although there is one subject that needs more explanation and that is Category theory. As one of the authors says:

“I think we did a fairly good job of not assuming too much background in topology and in type theory, but we did use a fair number of category-theoretic concepts without really explaining them in much detail”2

So it is a good idea to have an introduction to category theory. I don’t know much about category theory either, so if you do, and you want to contribute, please let us know by opening an issue on our GitLab.

With that being said, there is a great introductory video series on category theory by Steve Awodey on youtube: Category Theory Foundations, Lecture 1

1. Andrej Bauer (https://github.com/HoTT/book/issues/727, 2014).↩

2. Mike Shulman (https://github.com/HoTT/book/issues/733, 2014).↩

3 Category theory

This chapter contains an introduction to category theory. Category theory is one of the preliminaries to the HoTT book that isn’t discussed in much details. In this chapter we will try to give you a super simple foundation of it.

4 Type theory

4.1 Type theory versus set theory

Proposition: A statement susceptible to proof.

Theorem: A proposition that has been proven.

Deductive system: A collection of rules for deriving judgments.

Judgment (first order logic): For the proposition

Judgment (type theory):

Propositions are types: Finding an element of a type is proving that proposition. Thus we call an element of a type a witness or an evidence of the truth of a proposition.

Propositional equality: When

Judgmental (or definitional) equality: When two expressions are equal by definition. You expand and compute the definitions and conclude that they are equal. We write it as

Assumption:

Context: The collection of all such assumptions.

Type former: A way to construct types, together with rules for the construction and behavior of elements of that type.

For the rest of this chapter we will introduce these type formers:

- Function types

- Universes and families

- Dependent function types (

- Product types

- Dependent pair types (

- Coproduct types

- The type of booleans

- The natural numbers

- Pattern matching and recursion

- Propositions as types

- Identity types

- Path induction

- Equivalence of path induction and based path induction

- Disequality

English

Type Theory

True

False

If

Not

For all

There exists

How to introduce a new kind of type:

1. Formation rules: How to form new types of this kind.

2. Introduction rules (type’s constructors): How to construct elements of that type by:

- Direct definition

- When we don’t want to introduce a name for the function.

3. Elimination rules (type’s eliminators): How to use elements of that type.

4. Computation rule ( How an eliminator acts on a constructor.

5. Uniqueness principle ( Expresses the uniqueness of maps into or out of that type.

6. Propositional uniqueness principle (optional): When the uniqueness principle is not taken as a rule of judgmental equality, we can prove it as a propositional equality from the other rules for the type.

4.2 Function types

1. Formation rules: Given types

2. Introduction rules:

- Direct definition: Defining

3. Elimination rules: Given a function

4. Computation rule:

5. Uniqueness principle: uniquely determined by its values.

4.3 Universes and families

Universe: a type whose elements are types.

Hierarchy of universes:

Typical ambiguity: Omitting the level

Families of types: Using functions

4.4 Dependent function types

1. Formation rules: Given a type

2. Introduction rules:

- Direct definition: To define

3. Elimination rules: Applying

4. Computation rule: Given

5. Uniqueness principle:

Polymorphic function: A class of dependent function types which takes a type as one of its arguments and acts on elements of that type.

4.5 Product types

1. Formation rules: Given types cartesian product.

2. Introduction rules:

- Direct definition: Given

3. Elimination rules: For any

4. Computation rule:

5. Propositional uniqueness principle: Every element of

Unit type: We call the nullary product type the unit type

5 Homotopy type theory

“We seem to get a fair number of people who hit the beginning of chapter 2 and think”oh no, I don’t know what an Mike Shulman1

1. (https://github.com/HoTT/book/issues/740, 2014).↩

6 To Be Continued…

As I said in the Preface I’m currently reading the original HoTT book and this is a work in progress. So stay tuned and always check for the newest version at https://www.mehranbaghi.com/hott_for_cools/.

Bibliography

Bauer, Andrej. https://github.com/HoTT/book/issues/727, 2014.

Shulman, Mike. https://github.com/HoTT/book/issues/733, 2014.

———. https://github.com/HoTT/book/issues/740, 2014.

HoTT for Cools

1. 1 Preface

1. 1.1 Disclaimer

2. 1.2 How to Contribute

1. 1.2.1 List of Contributors

3. 1.3 Acknowledgment

4. 1.4 License

2. 2 Introduction

3. 3 Category theory

4. 4 Type theory

1. 4.1 Type theory versus set theory

2. 4.2 Function types

3. 4.3 Universes and families

4. 4.4 Dependent function types

5. 4.5 Product types

5. 5 Homotopy type theory

6. 6 To Be Continued…

7. Bibliography

1. Cover