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


7

Definitional equality is the same as equality in the metatheory. It works exactly the same way as in 1-category theory. If I have a category $\mathbb{C}$ and some morphisms $f,g : \mathbb{C}(A, B)$, I write $f = g$ for their equality, where $=$ is a metatheoretical relation. I can assume a family structure on $\mathbb{C}$ to get a CwF, plus assume some type ...


6

The basic idea is clearest when you think about things in terms of Tarski-style universes. There, you have a data type of codes, and an interpretation function which maps codes to types. In this case, it is obvious that you can discriminate on type codes, even though this is a much more questionable operation on types. For example, $\mathbb{N} \to 0$ and $\...


6

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


6

No: strong elimination of large inductive types (SELIT) is itself inconsistent because it breaks the layering of universes by trivially allowing you to smuggle a large value in a Prop box and take it back out unscathed. In Is Impredicativity Implicitly Implicit? I proposed a restriction on SELIT which is a bit more permissive than Coq's while still enjoying ...


4

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


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

U : U is inconsistent in a wide variety of settings. It is safe to say that it's inconsistent in any type theory. Deriving False from it is feasible by hand. The simplest version of this is called Hurkens' paradox: Original source Coq implementation. Agda implementation. The Coq source additionally describes the sufficient conditions for getting False. In ...


4

May I have a reference to why η expansion is invalid for CoC? It's not invalid. It's up to choice whether $\eta$-conversion for functions (or other types) is included. The original CoC paper seems to omit it, but as you see ATAPL includes it. I'm not certain, but $\eta$ may have been omitted from the original source because it was difficult to handle in the ...


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


4

Definitional equality is essentially a syntactic notion of equality, not witnessed by a term in the type theory: when two types or terms are definitionally equal, we are saying that they are precisely the same. Therefore, definitional equality of types is interpreted as equality of objects, and definitional equality of terms is interpreted as equality of ...


4

To me, type theory bridges programming with models and proof theories. In particular, I can use category theory to think about programming languages when the underlying type theory has a categorical model (e.g. the intuitionistic type theory by Martin Löf). On the other hand, type theory to programming is like (point-set) topology to analysis -- it gives you ...


4

Disclaimer: I've never actually implemented any variation of cubical type theories and I am not an expert in cubical type theory. I write this answer according to my own intuition. I welcome corrections and complementaries. How does this actually compute a path from a to d? The comp operator creates a term that has the following properties (in your case, ...


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

Here is one article that discussed induction-recursion. Here's their code: data Lang : Set ⟦_⟧ : Lang → Set data Lang where Zero One Two : Lang Pair Fun Tree : (A : Lang) (B : ⟦ A ⟧ → Lang) → Lang ⟦ Zero ⟧ = ⊥ ⟦ One ⟧ = ⊤ ⟦ Two ⟧ = Bool ⟦ Pair A B ⟧ = Σ ⟦ A ⟧ λ a → ⟦ B a ⟧ ⟦ Fun A B ⟧ = (a : ⟦ A ⟧) → ⟦ B a ⟧ ⟦ Tree A B ⟧ = W ⟦ A ⟧ ...


3

"Types are the leaven of computer programming; they make it digestible." Robin Milner


3

I think I just came up with one. The following code block is written in a syntax similar to Agda. test : (a : _) (B : Set) (b : B) -> a ≡ b test a B b = refl Assuming ≡ to be the homogeneous equality type and refl to be its constructor, the solution to the underscore is B, which is not defined there yet. Type checking the above code (with open import ...


3

They are different things. SClos is a case-split function, which is a function that pattern match on its parameter. Think of it as a lambda (if you know Haskell, you can think of it as a LambdaCase \case, which is a sugared lambda). This is definitely a canonical value in Mini-TT. The neutral value, OTOH, is an application on a case-split function, where the ...


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


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

It is false that the only well-typed occurrence of Prf has to be of the form Prf(all ...). For example, in the context with a variable p : Prop we can form the type Prf(p) which is not of the stated form. Another possibility is that we have a Prf(t) for some closed term t : Prop which is not of the form all ... but it normalizes to it. The purpose of Prf is ...


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


2

I don't have an answer for that question, I'm afraid. But I'll just point out that the rule you cite doesn't say that we should use Γ ⊢ e₁ e₂ ⇒ τ just because function application is an eliminator. Instead, it says that within the typing rule for function application, the part that checks the actual function should synthesize (i.e. should be Γ ⊢ e₁ ⇒ τ₁ → ...


2

IMHO, it's not like constructors are checked, but introduction rules (including tuples, lambdas, data constructors, etc.) are checked (while elimination rules are synthesized). The kind constructors you mentioned are called formation rules, which are not introduction rules. You can also think this way: if a constructor is checked, then it has a corresponding ...


2

No, but only under a very specific condition (neither MLTT, or CoC, or LF) -- that your type theory has certain resource control mechanism (linear or affine). See Affine logic Wikipedia entry. Affine logic predated linear logic. V. N. Grishin used this logic in 1974, after observing that Russell's paradox cannot be derived in a set theory without ...


1

IMHO universe hierarchy is particularly complicated to implement while the benefit is very small. It complicates programming in the language and the implementation of the language. The only benefit is to ensure the logical consistency. I guess that's why everybody is not writing about it. Here are some answers to your questions. I don't know much type theory ...


1

I have a shorter answer: normalization is usually used in conversion check of terms (aka definitional equality), and CoC has untyped conversion check. In conversion check, we normalize terms and compare 'em syntactically (think of it as comparing the ASTs). This probably means the normalization process doesn't have access to the types of terms, so it may not ...


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


1

Here is an example exploiting positivity of an index to prove false: module Whatever where open import Level using (Level) open import Relation.Binary.PropositionalEquality open import Data.Empty variable ℓ : Level A B : Set ℓ data _≅_ (A : Set ℓ) : Set ℓ → Set ℓ where trefl : A ≅ A Subst : (P : Set ℓ → Set ℓ) → A ≅ B → P A → P B Subst P trefl PA = ...


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