HOTT/UF PROGRAM
Days: Saturday, July 7th Sunday, July 8th
Saturday, July 7th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:30-10:30 Session 24A
Chair:
Location: Blavatnik LT1
| 09:30 | Axiomatizing Cubical Sets Models of Univalent Foundations (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 26F
Chair:
Location: Blavatnik LT1
| 11:00 | Internalizing Presheaf Semantics: Charting the Design Space (abstract)  |
| 11:30 | Cubical Assemblies and the Independence of the Propositional Resizing Axiom (abstract) |
| 12:00 | Dependent Right Adjoint Types (abstract) |
12:30-14:00Lunch Break
14:00-15:00 Session 28D: HRDA & HoTT/UF Invited Talk: Paige North (joint with HDRA)
Chair:
Location: Blavatnik LT2
| 14:00 | A homotopy type theory for directed homotopy theory (abstract) |
15:00-15:30 Session 30C
Chair:
Location: Blavatnik LT1
| 15:00 | Geometric realization of truncated semi-simplicial sets meta-constructed within HoTT (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 31F
Chair:
Location: Blavatnik LT1
| 16:00 | Univalent Foundations and the Constructive View of Theories (abstract) |
| 16:30 | Algebraic models of dependent type theory (abstract) |
| 17:00 | First-order homotopical logic and Grothendieck fibrations (abstract) |
19:45-22:00 Workshops dinner at Balliol College
Workshops dinner at Balliol College. Drinks reception from 7.45pm, to be seated by 8:15 (pre-booking via FLoC registration system required; guests welcome).
Location: Balliol College
Sunday, July 8th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
09:30-10:30 Session 36A
Chair:
Location: Blavatnik LT1
| 09:30 | Injective types and searchable types in univalent mathematics (abstract) |
10:30-11:00Coffee Break
11:00-12:30 Session 38H
Chair:
Location: Blavatnik LT1
| 11:00 | A Yoneda lemma-formulation of the univalence axiom (abstract) |
| 11:30 | Robust Notions of Contextual Fibrancy (abstract) |
| 12:00 | Cohesive Covering Theory (abstract) |
12:30-14:00Lunch Break
14:00-15:30 Session 40H
Chair:
Location: Blavatnik LT1
| 14:00 | Cubical Computational Type Theory (abstract) |
| 14:30 | The definitional symmetric cubical structure of types in type theory with equality defined by abstraction over an interval (abstract) |
| 15:00 | Ordered Cubes (abstract) |
15:30-16:00Coffee Break
16:00-18:00 Session 42G
Chair:
Location: Blavatnik LT1
| 16:00 | (Truncated) Simplicial Models of Type Theory (abstract) |
| 16:30 | Towards the syntax and semantics of higher dimensional type theory (abstract) |