12

It turns out that $W$ types plus identity types (eq/= in Coq) allow you to construct pretty much all the general inductive types you want, with the expected computation rules, and even canonicity. This is a very recent result of mine, you can read a preprint at Why not W?, which has been accepted for publication in the TYPES 2020 post-proceedings. The idea ...


8

Yes. System F is probably the simplest example. As far as I know, you can’t prove normalisation for it in a dependent type theory with induction-recursion — you need at least impredicative prop to do so.


8

This is not an answer but a very long comment. I find the idea quite interesting. To keep things focused, I think it would be very good to have a clear idea of what it means for the encoding of cubical type theory to be correct, namely that it is sound and conservative. Soundness just means you can encode everything (for instance, that you did not forget to ...


7

We are going to show that in MLTT with propositional truncation the type $$\textstyle \prod_{A:U_0}\prod_{B:U_0} (\|A\| \to A) \times (\|B\| \to B) \to (\|A + B\| \to A + B) $$ has no inhabitants. Assume it did. We shall work in a specific model of MLTT with propositional truncation, namely assemblies over number realizability. It is not too important what ...


6

The discussion in the section surrounding that paragraph in Pierce's book explains why this is so. In particular, consider the definition of "type system" given on the page before: A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute. ...


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 ...


5

DEDUCT_ANTISYM_RULE only applies to propositions, while REFL applies to all terms of all types. Your suggestion only shows that every propositions is equal (equivalent) to itself, but it could not be used to show that ever number equals itself.


5

As Andrej notes, $\lambda\Pi$ is a conservative extension of first-order logic which means: Adding the axioms of PA to $\lambda\Pi$ gives exactly the same arithmetic theorems as PA. However, because of the more expressive system, it is possible to finitely axiomatize induction using the following (encoding of) this axiom: $$ \forall P: {\mathbb N}\...


5

Uniqueness is not converse to introduction. Uniqueness rules in type theory are components of isomorphisms. If a type former is specified with an isomorphism, then Constructors form one map Eliminators form the inverse map β-rules express elim ∘ con = id η-rules (uniqueness) express con ∘ elim = id For example, function types are given as Tm Γ (Π A B) ≃ Tm ...


4

No, there can't be such a surjection. Here's how to derive a contradiction, if there is a surjective map $f : A \to U_n$, where $A:U_m$. Since $m\leq n$, we can pull $f$ back along the embedding $U_m \to U_n$. This gives a surjective map $f' : A' \to U_m$, and it is not hard to see that the type $A'$ is equivalent to a type in $U_m$. Thus we have a ...


4

Use an auxiliary type of positive natural numbers. data positive : Set where one : positive s0 : positive → positive -- multiply by 2 s1 : positive → positive -- multiply by 2 and add 1 data N : Set where zero : N pos : positive → N Supplemental: Another option, which I found on my whiteboard today (probably put there by Egbert Rijke months ago)...


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{...


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 $\...


3

$(F, F^R)$ is not necessarily a relational functor. Define $F : \text{Set} \to \text{Set}$ to be the identity functor on sets and functions, but let ${F_!}^R$ send all relations to the trivial relation. Then ${F_{\text{map}}^R}$ trivially holds (along with ${F_{\text{id}}^R}$ and ${F_{\text{comp}}^R}$ which always hold for any $F$, because of the proof-...


3

We certainly do not need very many $W$-types. If we also have universes, we only need one $W$-type, namely the natural numbers. For example, the UniMath library uses just the natural numbers and no other inductive types (if we discount the fact that standard types constructors, such as products and sum, are defined inductively in Coq).


3

Type inference for dependent type theory is undecidable in general, so what you're asking for is impossible. However, it is possible to separate the syntax into inferrable terms and checkable terms, and implement inference for the inferrable fragment. This is the approach taken by bidirectional typechecking. The paper on LambdaPi by Andres Löh, Conor McBride ...


3

Take any small symmetric monoidal category $V$. Then the category of $V$-valued presheaves will (a) have closed monoidal structure (via Day convolution), and (b) have enough stuff (inherited from $\mathrm{Set}$) to interpret dependent types. This gives you enough structure to interpret something like our LNL calculus pretty easily, because there is a nice ...


3

If you intend to formalize meta-theorems in a proof assistant, then it's probably better to avoid the general weakening rule because it will pollute all your inductive arguments. Every single induction on the derivation will contain the case "but what if the context got larger using weakening?" and that's going to be super annoying. I would ...


3

But it does follow. The types $$A = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ n\ m)$$ and $$B = \prod_{(n,m:\textrm{Nat})}(\textrm{plus}\ n\ m) = (\textrm{plus}\ m\ n)$$ are both contractible. Indeed, they are both inhabited and because $\mathrm{Nat}$ is a set, its identity type is a proposition, hence so are $A$ and $B$, as they are ...


3

Łukasz Lew and Neel Krishnaswami are right; quotation is well-defined only for terms in normal form. This excludes recursive programs in traditional lambda-calculus but not in combinatory logic, since its naive interpretation of lambda-abstraction always produces normal forms (by breaking all redexes). Now that quotation is well-defined, we can ask if it is ...


3

I tried to address the questions you raise in "Five stages of accepting constructive mathematics". And here are some textbooks: Constructive analysis by D. Bridges and E. Bishop is the "bible" of constructive mathematics. Varieties of constructive mathematics by D. Bridges and F. Richman considers several varieties of constructive ...


2

I can't give you a (easily translatable) answer to the question regarding Haskell and the types, but the following might help you since you already mentioned ZFC: Take the axioms of ZFC and let's assume that ZFC is consistent. By the Löwenheim-Skolem Theorem Downwards (as a corollary to the Completeness Theorem for First-Order Predicate Logic) there is a ...


2

There are a number of ways to see HOL as an instance of a "dependent" type theory, in a way that is reasonable, that is there is a pure type system (https://en.wikipedia.org/wiki/Pure_type_system) $\mathrm{\lambda HOPL}$ which contains an embedding $$ [\!| \_\mid\!] :\mathrm{HOL}\rightarrow \mathrm{\lambda HOPL}$$ Which is both sound and complete, that is: ...


2

HOL is a simple type theory, while Martin-Löf's is a dependent type theory. That is the fundamental difference between the two. One can embed HOL into extensional type theory, i.e., type theory with identity types and the equality reflection principle $$\frac{\vdash p : \mathrm{Id}_A(s,t)}{\vdash s \equiv_A t}$$ You could try a less drastic principle, such ...


2

Addressing the question in the title: $\mathsf{\lambda n\,m.\,refl}$ is not a proof of commutativity by definition because addition is not a constant function by definition. Of course, the commutativity proof can be shown to be propositionally equal (by a "dependent" equality, or path-over-path) to the $\mathsf{refl}$-returning one, by Andrej's ...


2

Generally, there will be one context-free grammar for both types and terms, and judgements will be used to identify those expressions which are types and which expressions are terms of a particular type. This has been written down many, many times. For a pretty typical example, you could look at Abel, Coquand and Dybjer's LICS 2007 paper, Normalization by ...


2

As an inhabited proposition $(W_{a:A}B(a)\to 0)\to 0$ has only one term in normal form. First, without function extensionality, this type cannot be proven to be propositional. Second, propositional types do not necessarily have unique normal forms. Normal forms are up to $\beta\eta$ rules, not propositional equality. $0 \to 0$ has infinitely many normal ...


2

You asked several questions. You asked about a type indexed by a list, so you can do this. data DataType (A : Type) (F : A -> Type) : List A -> Type where empty : DataType A F [] _bla_ : forall {xs} {x} -> DataType A F xs -> F x -> DataType A F (x ∷ xs) Where F is a type family that is indexed by the elements of the list. Apart from that, ...


1

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.


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 ...


Only top voted, non community-wiki answers of a minimum length are eligible