Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [type-theory]

The tag has no usage guidance.

6
votes
2answers
402 views

How can the simply typed lambda calculus be Turing-incomplete, yet stronger than second-order logic?

It is well-known that the simply typed lambda calculus is strongly normalizing (for instance, Wikipedia). Hence, it is not strong enough to be Turing-complete, as also mentioned on the Wikipedia page ...
3
votes
0answers
194 views

Formal foundations done properly [closed]

I would want to do mathematics properly, so that the proofs of results can be trusted on instead of them being just suggestions on which results could perhaps apply. This means formulating the math in ...
12
votes
1answer
502 views

A peculiarity of Henkin's 1950 proof of completeness for higher order logic

My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models. ...
5
votes
1answer
277 views

Progress towards a computational interpretation of the univalence axiom?

I will preface this by saying that I am not an expert on type theory. I am just a curious outsider slowly making my way through the HoTT book when I (rarely) have some spare time. I am just curious ...
6
votes
1answer
317 views

Proof of ¬(¬1 ⊗ ¬1) in tensorial logic

I believe I once had a proof of this proposition, but it's been lost to the mists of time and old hard drives, so who knows if it was correct, and try as I might I can't seem to reproduce it. Is it ...
3
votes
1answer
96 views

Internal equality for Eq-fibrations' morphisms

I have posted this question here on M.SE but since it received little attention and since it seems difficult to find helpfule references I reposting it here. In Jacob's Categorical logic and Type ...
8
votes
4answers
801 views

Formalizations of the idea that something is a function of something else?

I'll state my questions upfront and attempt to motivate/explain them afterwards. Q1: Is there a direct way of expressing the relation "$y$ is a function of $x$" inside set theory? More ...
8
votes
0answers
222 views

What metatheory proves cut elimination for Simple Type Theory?

Gaisi Takeuti's book Proof Theory proves cut elimination for Simple Type Theory (a combined result of several researchers). Thus it proves consistency of Simple Type Theory with full comprehension in ...
7
votes
0answers
360 views

what's the point of cubical type theory?

I have been following through the development of homotopy type theory since 2013 because I was really interested in the foundation of mathematics. The novel idea of combining programming with homotopy ...
2
votes
1answer
167 views

Can a type in a lower universe be formed from types in higher universes?

A type universe is a type of small types that is closed under the basic type formation operations (dependent product, sum, coproduct etc.), that is to say for example that from $A \colon U_i$ and $x \...
2
votes
0answers
137 views

What is the consistency limit of accumulative typing below $\omega_1^{CK}$?

Let $Th_\zeta$ be a Mono-sorted first order theory with $\zeta$ representing some recursive ordinal notation system. Primitives: =, $\in$, $T_0, T_1, ..,T_i,..$ where i is an $\zeta$ ordinal, and ...
2
votes
0answers
61 views

What is the relation of total functions in second order arithmetic and fast growing hierarchies?

Answer to this questions shows that fast growing hierarchies can grow arbitrarily fast for some definition of 'arbitrary'. Can second order arithmetic define all these functions (for any ordinal) ...
13
votes
2answers
665 views

What kind of category is generated by Cubical type theory?

What kind of ‘category’ is Cubical type theory the internal language of? Its known that Martin-Löf type theories are the internal language of Locally cartesian closed categories, adding higher ...
3
votes
2answers
203 views

Stability and complete types (in Model Theory)

I read the following statement in these slides of Saharon Shelah: "$K$ is stable iff for every $M \in K$ there are only "few" complete types over $M$." About the notation: here $K$ consists of all ...
16
votes
1answer
751 views

New articles by Errett Bishop on constructive type theory?

Recently two formerly unknown articles by Errett Bishop (1928-1983) were posted online by Martín Escardó. One is entitled "A general language", deals with constructive type theory, and ...
1
vote
1answer
142 views

Is Calculus of Constructions type inhabitance semi-decideable?

I'm wondering if type inhabitance for the calculus of constructions is semi-decideable. I know the following: System F inhabitance and, correspondingly, second-order unification are semi-decideable ...
3
votes
0answers
85 views

Was Martin-Löf inspired by Peirce when he introduced the dependent sum and dependent product types?

In the following article: https://plato.stanford.edu/entries/peirce-logic/ it is mentioned that Peirce's introduced the use of the symbols $\Sigma$ and $\Pi$ to express logical sums and products, ...
5
votes
1answer
121 views

Propositional vs Definitional extentionality in type theory

There are essentially two ways to impose extentionality on a type theory (I know, it is not very fashionable to impose extentionality these days, but please, bear with me) you can either have a "...
15
votes
1answer
1k views

In constructive mathematics, why does the category of abelian groups fail to be abelian?

I was reading the paper Towards Constructive Homological Algebra in Type Theory by Thierry Coquand and Arnaud Spiwack, and they state that constructively, the category of abelian groups fails to be ...
5
votes
0answers
235 views

What does first-order co-intuitionistic logic look like (and does it have an equivalent type theory)?

So, this is where I'm at so far: Heyting algebras model propositional intuitionistic logic (IL) so do Cartesian closed categories which also model the simply typed lamda calculus co-Heyting algebras ...
7
votes
3answers
296 views

How to handle sums in Tait's reducibility proof of strong normalisation?

I've been reading Girard et al's 'Proofs and Types', which in Chapter 6 presents a proof of strong normalisation for the simply typed lambda calculus with products and base types. The proof is based ...
19
votes
1answer
1k views

Can you have a type theory where there is type of all types?

Normally in a type theory, you can not have a type of all types, due to Girad's paradox. This is somewhat similar to how in set theory, you cannot have a set of all sets. Therefore, usually you just ...
7
votes
0answers
141 views

Generalized (co)-presheaves for Generalized Multicategories?

A $T$-multicategory in the sense of Crutwell-Shulman, where $T$ is a monad on a virtual double category $C$ is a monoid in the "horizontal kleisli category", i.e., an object of objects $O$, a ...
6
votes
1answer
711 views

Rice's theorem in type theory

From the formula $$\forall f\colon A\to A\,\exists x\colon A\,(f(x)=x)$$ we can get the scheme $$\forall x\colon A\,(\phi(x)\vee\neg\phi(x))\Rightarrow\forall x\colon A\,\phi(x)\vee\forall x\colon A\,\...
4
votes
3answers
344 views

Homotopy type theory: Are the hierarchy of Type_k universes isomorphic?

In homotopy type theory, or dependent type theories more generally, there is a "top-level" type called the universe, generally denoted $\newcommand{\type}{\mathtt{Type}}\type$. So for a concrete ...
2
votes
1answer
255 views

Why are types in type theory unordered collections?

Please excuse my naïveté, I have no higher math education, just a curious observer. In type theories, types are treated as set-like because they're unordered collections. Yet, the putative motive in ...
23
votes
5answers
2k views

How do we construct the Gödel’s sentence in Martin-Löf type theory?

In Martin-Löf dependent type theory (MLTT), under the proposition-as-types correspondence, we sometimes say that a proposition $A$ is true if the type $A$ is inhabited. However, there is no doubt that ...
3
votes
1answer
169 views

Substructural types, the lambda calculus, and CCCs

It's well known that the simply-typed lambda calculus corresponds to a cartesian closed category. How would substructural type systems be characterized in category theory? For example, linear type ...
5
votes
2answers
688 views

Is simply typed lambda calculus with fixed-point combinator Turing-complete?

There are many sources cite that simply typed lambda calculus extended with fixed-point combinator is Turing complete. For example, Does there exist a Turing complete typed lambda calculus? or the ...
8
votes
0answers
168 views

Ends and parametricity

It is well known that a set of natural transformations can be expressed as an end: $$\int_{A \in \mathcal{A}} \mathcal{B}(FA, GA) =_{\operatorname{Set}} \operatorname{Nat}(F, G)$$ This holds for ...
19
votes
3answers
1k views

Why would the category of sets be intuitionistic?

This question is probably really naive. And, I hope the title doesn't come off as too combative. I think that topoi of $\mathbf{Set}$-valued sheaves provide an excellent motivation for higher-order ...
6
votes
1answer
247 views

Pure first order logic formulations of Markov's principle

Markov's principle is a statement of constructive arithmetic that allows classical reasoning on formulas of the shape $\exists x P$ when $P$ is a recursive predicate: $\neg \neg \exists x P \to \...
5
votes
2answers
701 views

What exactly is a judgement?

Before formulating my question, let me briefly sum up what I know about the topic (feel free to correct me if something I claimed is false!). This is for you good to see what my state of knowledge is, ...
8
votes
3answers
432 views

What is the definition of computational content?

I am interested in type theory and proof theory. I have read a lot of papers and books that use the term "computational content" (For example: https://scholar.google.com/scholar?hl=en&q=%...
3
votes
1answer
225 views

Are there types with nontrivial paths in all dimensions? (HoTT)

I'm trying to construct a model of homotopy type theory, and in my development it seems like it would be helpful to assume that all types only have trivial paths below a given level (forgive my ...
3
votes
0answers
390 views

New foundation in homotopy type theory

Is there any model of NF (New Foundations) on HoTT (homotopy type theory)? Because there is a model of ZF(C) on HoTT (The HoTT book, Section 10.5) and NF on ZFC (by this Wikipedia articile), I think ...
5
votes
1answer
377 views

Uniqueness Principle for function types

I am currently trying to understand the first chapter of the HoTT book and for 1.2 Functions Types of the book, Since it is by definition ``the function that applies $f$ to its argument'' we ...
12
votes
3answers
1k views

History of the notation for substitution

One of the very common notations for syntactic substitution is $[\ /\ ]$. However, there seems to be an inconsistency in the literature about its usage. Many write $[t/x]$ for "substitute $t$ for $x$...
5
votes
1answer
341 views

What do we call this quantifier (“binder”)?

There's a quantifier ("binder", whatever), call it $\alpha$, defined as follows: $\alpha x.\tau$ is the (usually infinite) expression obtained by applying the substitution $\{x \mapsto \tau\}$ to the ...
5
votes
0answers
192 views

Proper full submodels of full models of type theory

Let $N$ be the standard full model of the simply typed lambda calculus with infinite base type $o$ and let $X$ be an infinite and coinfinite subset of $N(o)$. I want to know if there's a full ...
3
votes
0answers
132 views

Internal language type of power objects

It is a basic fact that in a category with finite limits the following are equivalent Each object $X$ has a (membership relation to a) power object $PX\times X\hookleftarrow\ni_X$ subject to the ...
3
votes
0answers
184 views

Understanding Strong Normalization for Identity Types in Martin-Löf Intensional Type Theory [closed]

Roughly, the strong normalization property for Martin-Löf Intensional Type Theory (MITT) tells us that every closed term $t$ of type $M$ will eventually reach a canonical normal form $t’$ such that it ...
6
votes
1answer
289 views

Easier Girard's paradox in a circular pure type system (PTS)

System U is an inconsistent PTS in that one has a term of type $\bot = \forall p\colon \ast \ldotp p$, and such a term is explicitly constructed in Hurkens' A Simplification of Girard's Paradox. One-...
7
votes
2answers
609 views

Identity types: What makes Intuitionistic Type Theory *intuitionistic*?

In the opening passage of Martin-Löf's (1975) he famously says that "the theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic ...
14
votes
1answer
460 views

Why the reflection rule trivializes higher paths in Martin-Löf Extensional Type theory?

Martin-Löf Extensional Type theory differs from its intensional counterpart in that it contains the so-called reflection rule that says that if $p : x = y$, then actually $x \equiv y$ (i.e. $x$ and $y$...
3
votes
2answers
391 views

In a fibration, where does the generic object live?

In Bart Jacobs. Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics 141. North Holland, 1999. isbn: 9780444508539, the author writes, p. 326: Sometimes, for ...
2
votes
2answers
238 views

type theory that does not treat the terms of $\mathrm{Prop}$ as types

In type theory there is a type $\mathrm{Prop}$ that contains every proposition, so $p\colon\mathrm{Prop}$ (in words, "$p$ is of type $\mathrm{Prop}$") where $p$ is a proposition. In all type theories ...
18
votes
1answer
3k views

What is the most transparent, rigorous definition of the Univalence Axiom?

I've been studying homotopy type theory and trying to grasp the Univalence Axiom. I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers ...
6
votes
1answer
249 views

On an automatic translation of typed lambda calculus in untyped lambda calculus

I have a question regarding the "compilation" of typed lambda calculus in untyped lambda calculus. Take for example the inductive definition of lists, with introduction rules: and: We can ...
2
votes
0answers
163 views

Type theory: can multiple elimination rules be defined, in principle?

I'd like to ask a question on type theory: Consider the usual type theoretical definition of the natural numbers. We could give an elimination rule in the form: or in the form: I called the ...