New answers tagged dependent-type
1
The principle of propositions-as-types (or formulas-as-types), also known as the Curry-Howard correspondence, is the key idea for viewing (intuitionistic) type theories as logical systems and to apply type theories (and constructive mathematics in general) to computer science.
Suppose U is the type of all propositions, then U is also the type of all types by ...
4
$\text{absurd} : (A : \text{U}) \to 0 \to A$ and $\text{elim} : (A : 0 \to \text{U}) \to (x : 0) \to A\,x$ are equivalent. To go right, use $\text{absurd}\,(A\,x)\,x$. To go left, use $\text{elim}\,(\lambda\,x.\,A)\,x$. Also, both types are propositions because of the $0$-s in domains. There's not much reason to assume or use $\text{elim}$ instead of $\text{...
0
Ali Asaf worked out a hierachy of universes with explicit coercions (lifting) in A calculus of constructions with explicit subtyping and established a relationship with cummulative universes.
0
I haven't found a clear set of rules for such a system (including for Agda, tho the source code admittedly should count), so in my paper Is Impredicativity Implicitly Implicit?. I wrote what I understand of Agda's rules (and according to one of the reviewers it's about right).
But I don't know what you mean by "the rules for the universe lifting ...
3
This is impossible.
Suppose that we have such a type $T$, with an implementation of addition $\mathit{add} : T \to T \to T$, which is judgementally commutative.
Because MLTT is strongly normalising, we know that we can put $\mathit{add}$ in $\beta$-normal, $\eta$-long form.
Now suppose that we have two variables $x, y$ of type $T$.
Now consider the terms $\...
1
CoqMT (Coq Modulo Theory) was an extension of the Coq proof assistant that allows one to parametrize a development with a decidable first-order theory T. Since equality on natural number expressions with addition and multiplication is decidable, this would be a valid application of CoqMT. Unfortunately, the implementation has not been updated in over 10 ...
5
The simplest one that I know about is the $\text{Set}$-based polynomial model ("container" model). Here, every context is interpreted as a family of sets, i.e. a $Q : \text{Set}$ together with an $A : Q \to \text{Set}$. We can view this as a set of questions together with sets of possible answers for each question, or a request-response protocol ...
Top 50 recent answers are included
