Questions tagged [type-theory]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
7
votes
0answers
248 views

Feasible Type Theories

I am looking for references about efficient type theories, efficiency in the sense of computational complexity, and type theory in the sense of Martin-Lof's type theories. Has there been any studies ...
6
votes
2answers
864 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, ...
6
votes
4answers
875 views

What is the intuitive meaning of star and box in a pure type system?

The systems of the λ-cube have the axiom $\star:\square$. I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and $\...
6
votes
1answer
1k views

What fails when using call/cc as realizer of the Peirce formula

Define the axiom constants $p_{A,B}^{((A\rightarrow B)\rightarrow A)\rightarrow A}$ as realizers of the Peirce formula, and $f_A^{\bot\rightarrow A}$ as realizers of the Ex Falso Quodlibet. Then $p_{A\...
6
votes
2answers
318 views

Why no morphisms from the contradictory proposition to the inconsistent context?

Consider Higher order predicate logic over dependent type theory (DPL) as defined in Chapter 11 of B. Jacobs's book "Categorical Logic and Type Theory" (though I think this question applies to first-...
6
votes
2answers
846 views

Recursively dependent types?

Is there such a thing as "recursively dependent types"? Specifically, I would like a dependent type theory containing a type $A(x)$ which depends on a variable $x: A(z)$, where $z$ is a particular ...
6
votes
1answer
340 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 ...
6
votes
1answer
739 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\,\...
6
votes
1answer
270 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 ...
6
votes
2answers
204 views

When is a fold monomorphic/epimorphic

Given a functor $F : \mathcal C \to \mathcal C$ with initial algebra $\alpha : FA \to A$, and another algebra $\xi : FX \to X$, we obtain a unique morphism $\mathsf{fold}~\xi : A \to X$ such that $\...
6
votes
1answer
270 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 \...
6
votes
1answer
401 views

$\Pi$, $\Sigma$, and identity types without $\eta$ in comprehension categories

In comprehension categories, dependent sums are defined as a choice of left adjoints for all reindexing functors along display maps, satisfying a Beck-Chevalley condition. Dependent products are ...
6
votes
1answer
622 views

What notions of universe does predicative type theory admit?

Palmgren (1997), On universes in type theory, discusses work of several theorists that provide what we might call a family of Large Universe Axioms (LUAs) for predicative type theory, culminating in ...
6
votes
0answers
277 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 ...
6
votes
0answers
152 views

Preservation of universes in presheaves

In Lifting Grothendieck universes Hofmann and Streicher construct a universe in the category of presheaves over a small category given a Grothendieck universe in $\mathbf{Set}$. Suppose now I have ...
5
votes
2answers
703 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 ...
5
votes
1answer
351 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
1answer
465 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 ...
5
votes
1answer
385 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 ...
5
votes
2answers
530 views

Question about higher inductive types and computational rules

I have been trying to make my way through the homotopy type theory book, slowly but surely, and I just finished reading this introductory series of 3 articles on hott on ScienceForAll. http://www....
5
votes
1answer
129 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 "...
5
votes
0answers
174 views

Are any formal systems based upon the idea of “iterated characterization pushing” currently in existence? If not, is anyone working on them?

I had an idea in regards to the design of formal systems with foundational aspirations. To convey the idea, let's talk a bit about the second-order Peano axioms. The way these axioms work, we have a ...
5
votes
0answers
195 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 ...
4
votes
3answers
372 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 ...
4
votes
3answers
599 views

Can a typing judgment admit essentially different derivations?

In any sort of type theory, there are a bunch of rules for constructing derivations of typing judgments such as $x:A,\; y:B(x) \;\vdash\; z:C(x,y)$. (I intend to include also judgments of the form $B:...
4
votes
1answer
287 views

Uniqueness principle for functions types in the HoTT book

Chapter 1.2 of the HoTT book says this about eta-conversion: $$ f \equiv (\lambda x . f(x)). $$ This equality is the uniqueness principle for function types, because it shows that $f$ is uniquely ...
4
votes
2answers
265 views

Is there a name for relations with this property, and the category of them?

The following math.stackexchange question asked whether there is a name for a certain sort of relation. I have become interested in the question, and no one suggested a name there, so I am asking ...
4
votes
1answer
407 views

What are categorical models of W-types in intensional type theory?

I'm familiar with container functors and older work by Dybjer on categorical models for W-types in the extensional theory, but I was looking for some similar semantics in the intensional case.
4
votes
0answers
421 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 ...
4
votes
0answers
116 views

Problem with a proof in Wellfounded trees in categories

I'm reading the paper Wellfounded trees in categories by Moerdijk and Palmgren. I'm having trouble understanding the proof of Theorem 7.2 (page 216), i.e. that in $\mathbf{ML}_{< \omega} \mathbf{W}$...
3
votes
1answer
235 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
2answers
417 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 ...
3
votes
2answers
241 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 ...
3
votes
1answer
243 views

Type with $X\rightarrow X\cong X + 1$

In the article Voevodsky’s Univalence Axiom in Homotopy Type Theory, an example is given of how types are not like sets: the existence of a nontrivial (nonzero) type $X$ such that $X\rightarrow X\...
3
votes
1answer
108 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 ...
3
votes
1answer
195 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 ...
3
votes
0answers
249 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 ...
3
votes
0answers
98 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, ...
3
votes
0answers
144 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
202 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 ...
3
votes
0answers
149 views

Logical framework for type theories like ML and CIC

I'm looking for a logical framework in which it is possible to easily present both intensional and extensional theories of dependent types with a partially ordered set of universes à la Russell ...
3
votes
0answers
202 views

An elegant formulation for typed sets

Fix a poset $T$, which we'll think of as a set of "types," interpreting $a \leq b$ as "$a$ is more general than $b$." Construct a category of TSet as follows. Objects: Pairs ($X$, $\tau : X \...
2
votes
2answers
247 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 ...
2
votes
2answers
1k views

What is a semigroup or, what do I do with that associativity proof?

Mathematically, I know what a semigroup is: It is a set S along with an associative binary operation $* : S \times S \rightarrow S$. So far, so good. From a computational perspective, one can ...
2
votes
1answer
254 views

Relation between different definitions of types [closed]

Is there any connection between the definition of type in model theory and the definitions from type theory? Is there any explanation why the same term is used for these notions, maybe in the ...
2
votes
1answer
184 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
1answer
273 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 ...
2
votes
1answer
188 views

Is there research on the notion of co-accessibility?

I want to start off with a disclaimer that I am only a mathematical amateur. Please forgive me for ignorance or any non-standard nomenclature I use here :) Let's start off with some context. Let X ...
2
votes
0answers
133 views

Categorical semantics of the identity type

In Appendix B of the article Simplicial Model of Univ. Foundations, Definition B.1.3 specifies the structure for identity types in a contextual category $\mathcal{C}$ (which in particular is equipped ...
2
votes
0answers
151 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 ...