Séminaire, 11 février 2016

Programme

10:30 – 12:00

Thorsten Altenkirch (University of Nottingham (UK))

Invited talk: What is a category? (in univalent type theory)

Category theory is one of the main tools in theoretical computer science. Univalent type theory allows us to represent ordinary category theory in a very straightforward way but we need to assume that the hom-types are sets in the sense of univalent type theory, that is their equalities are mere propositions. In my talk I a going to explore how we can lift this limitation and how we can define (\omega,1)-categories in a 2-level type theory. The 2-level theory is necessary because we have to distinguish between strict and weak equality and consequently between types and pretypes. One application of this approach is a generic theory of higher inductive types.

This is based on ongoing work with Paolo Capriotti, Gabe Dijkstra, Frederik Forsberg and Nicolai Kraus.

14:00 – 15:00

Simon Boulier (INRIA)

Invited talk: Model structure in Homotopy Type Theory

Homotopy Type Theory is conjectured to be the internal language of (∞,1)-topoi. In particular, the category of contexts of HoTT is an (∞, 1)-category. This (∞, 1)-cateory can be presented as a category with weak equivalences, where weak equivalences are given by the now customary type theoretic equivalences. But we can add more structure: namely we can define what are fibrations and cofibrations in type theory, so that the category of contexts be a model category. This was done by Gambino and Garner [GG] and Lumsdaine [Lum] and we will start by presenting their work.

Next we will consider moving to a two level type system like the one considered by Thorsten Altenkirch, to formalize those notions internally. Indeed, a strict equality satisfying UIP allows to formalize what is a strict category and a model structure over it.

Last, we will see how the model structure justify some homotopy colimit calculations from strict colimits.

[Lum] Lumsdaine, P. L. (2011). Model structures from higher inductive types. http://peterlefanulumsdaine.com/research/Lumsdaine-Model-strux-from-HITs.pdf.

[GG] Gambino, N., & Garner, R. (2008). The identity type weak factorisation system. Theoretical Computer Science, 409(1), 94-109.

• slides of the presentation

15:30 – 16:30

Nicolas Tabareau (INRIA, inventeurs du monde numérique)

Invited talk: Enlarge your Coq using Forcing.

We will study forcing translations of proofs in dependent type theory, through the Curry-Howard correspondence. Based on a call-by-push-value decomposition, we will synthesize two simply-typed translations: i) one call-by-value, corresponding to the translation derived from the presheaf construction as studied in a previous pa- per; ii) one call-by-name, whose intuitions already appear in Krivine and Miquel’s work. 

Focusing on the call-by-name translation, we will adapt it to the dependent case and prove that it is compatible with the definitional equality of our system, thus avoiding coherence problems. This allows us to use any category as forcing conditions, which is out of reach with the call-by-value translation. Our construction also exploits the notion of storage operators in order to interpret dependent elimination for inductive types. This is a novel example of a dependent theory with side-effects, clarifiying how dependent elimination for inductive types must be restricted in a non-pure setting. Being implemented as a Coq plugin, this work gives the possibility to formalize easily consistency results, for instance the consistency of the negation of Voevodsky’s univalence axiom.

Finally, if time allows, we will see how the forcing translation could give rise to a computational of the univalence axiom using the category of cubes as forcing conditions and interpreting the cubical type theory of Coquand et al.