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.