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
Related Tags
dependent-type × 96type-theory × 77
lo.logic × 17
pl.programming-languages × 17
typed-lambda-calculus × 15
lambda-calculus × 14
type-systems × 13
coq × 13
reference-request × 10
calculus-of-constructions × 8
proof-assistants × 6
ct.category-theory × 5
agda × 5
functional-programming × 4
homotopy-type-theory × 4
type-inference × 3
inductive-type × 3
automated-theorem-proving × 2
program-verification × 2
curry-howard × 2
cc.complexity-theory × 1
pr.probability × 1
proof-theory × 1
formal-methods × 1
set-theory × 1