Logic Seminar - Steve Awodey

January 8, 2019
Tuesday, February 5, 2019 - 1:45pm to 3:00pm
University Hall 082
Steve Awodey

Title: Impredicative encodings in homotopy type theory

Speaker: Steve Awodey (Carnegie Mellon)

Abstract: We present some recent results on impredicative encodings of inductive types (including higher inductive types) in HoTT. It is well-known that encoding inductives using higher-order quantification (i.e. quantification over all types) provides a potential theoretical and practical simplification of the type system. Using the further resources available in HoTT permits a sharpening of the usual System F style, impredicative encodings, but this begs the question of whether impredicativity is compatible with univalence. We give a realizability model using a combination of topos-theoretic, homotopical, and recent cubical methods. (Joint work with Jonas Frey and Pieter Hofstra.)

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