New answers tagged

4

Skolemization corresponds to the so-called type theoretic axiom of choice, which is briefly discussed in section 1.6 of the HoTT book. This provides an equivalence along which we can swap $\Sigma$ and $\Pi$ types. Assuming $A : U$, $B : A \to U$ and $C : \prod_{a : A} B\,a \to U$, we have an equivalence: $$ac : \Big(\prod_{a : A}\sum_{b : B\,a}\,C\,a\,b\...


6

You should have a look at the following paper -- and the previous work by Gori and Levi: On Polymorphic Recursion, Type Systems, and Abstract Interpretation Marco Comini1, Ferruccio Damiani2, Samuel Vrech, 2008 The problem of typing polymorphic recursion (i.e., recursive function definitions rec {x = e} where different occurrences of x in e are used ...


Top 50 recent answers are included