University COVID-19 update

The University of Waterloo is constantly updating our most Frequently Asked Questions.

Questions about buildings and services? Visit the list of Modified Services.

Please note: The University of Waterloo is closed for all events until further notice.

Homotopy Type Theory SeminarExport this event to calendar

Thursday, September 13, 2018 — 3:00 PM EDT

John Dykes, Department of Pure Mathematics, University of Waterloo

"Homotopy Type Theory and Univalent Foundations: Lecture 2"

Continuing from where we left off last week, we review function types. In discussing dependent pair and function types, we introduce the lambda calculus. We see the analogues of some standard set-theoretic constructions (products and coproducts, booleans, natural numbers) in the context of type theory. Using the analogy between propositions and types, we demonstrate how the axiom of choice can be (naively) rewritten as a type-theoretic statement. Time permitting, we  explain how the concepts of recursion and induction come alive in the type theory setting.

MC 5413

S M T W T F S
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
1
2
3
4
  1. 2020 (64)
    1. March (16)
    2. February (26)
    3. January (22)
  2. 2019 (199)
    1. December (7)
    2. November (26)
    3. October (19)
    4. September (13)
    5. August (7)
    6. July (12)
    7. June (18)
    8. May (22)
    9. April (11)
    10. March (25)
    11. February (17)
    12. January (22)
  3. 2018 (219)
  4. 2017 (281)
  5. 2016 (335)
  6. 2015 (209)
  7. 2014 (235)
  8. 2013 (251)
  9. 2012 (135)