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.

8
votes
0answers
223 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 ...
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 ...
7
votes
0answers
408 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 ...
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 ...
7
votes
0answers
238 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
0answers
150 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
0answers
237 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 ...
5
votes
0answers
193 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
0answers
396 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
115 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
0answers
86 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
133 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
146 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
201 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
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) ...
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 ...
1
vote
0answers
81 views

Natural relations between substitutions

Consider two contexts $\Gamma,\Delta$ (from some background type theory), and substitutions $s_1,s_2:\Gamma\rightarrow \Delta$. In the case of $1$-element contexts, we get that a substitution is ...