Questions tagged [type-theory]
The type-theory tag has no usage guidance.
51
questions with no upvoted or accepted answers
25
votes
0
answers
5k
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 ...
- 411
10
votes
0
answers
307
views
Feferman's universes for proof assistants?
This question was prompted by a discussion from another MO question about the consistency of ZFC. There are some mathematicians who are comfortable with ZFC but uneasy with large cardinals. For them,...
- 78.3k
9
votes
0
answers
410
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 ...
- 10.8k
8
votes
0
answers
94
views
Adjoining a morphism to a finitely complete category
Let $\mathscr C$ be a finitely complete category. Let $x, y$ be objects of $\mathscr C$. We can describe the universal property of freely adjoining a morphism $x \to y$ to $\mathscr C$: it comprises a ...
- 8,755
8
votes
0
answers
322
views
Curry-Howard isomorphism: What is the logical counterpart of closure conversion?
Continuation-Passing Style (CPS) translation in programming languages corresponds to double-negation translation in logic (and the Yoneda lemma in category theory). Then what in logic corresponds to ...
- 193
8
votes
0
answers
171
views
Does the "coproduct-elimination transform" have an accepted name, and where can I learn more about it?
Suppose we're in a bicartesian closed category. Then given a morphism $$f : X \rightarrow Y_1 + \ldots + Y_n$$ and a test object $T$, we get a corresponding morphism
$$T^f : X \times [Y_1,T] \times \...
- 3,693
8
votes
0
answers
187
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 ...
- 827
8
votes
0
answers
218
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 ...
- 5,535
7
votes
0
answers
167
views
Constructive theory of Lie algebras
I'm looking for references on constructive Lie algebra theory, e.g. the sort of theory you could develop in Martin-Löf type theory or internal to some topos with a NNO. Obviously excluded middle is ...
- 5,933
7
votes
0
answers
234
views
New Foundations in a Homotopy/Intuitionistic Type Theory form?
New Foundations is a famously odd set theory suggested by Quine in the 1930s which:
Features a universal set.
Disproves the axiom of choice.
Proves the existence of an infinite set by a trivial ...
- 4,843
7
votes
0
answers
294
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 ...
- 5,362
6
votes
0
answers
278
views
Is there any reason not to use Hofmann-Streicher universes?
Let $\mathcal C$ be a small category, and consider the topos $Psh(\mathcal C)$ of $Set$-valued presheaves on $\mathcal C$. For simplicity, assume that there exists a proper class of inaccessible ...
- 61.5k
6
votes
0
answers
330
views
More rigorous presentations of Martin-Löf type theory?
I'm enjoying reading Martin-Löf's 1972 paper "An Intuitionistic Theory of Types" for the first time (this constitutes my first-ever exposure to Martin-Löf's papers), but at times find the &...
- 505
6
votes
0
answers
156
views
Inductive type constructors with the defined type appearing in non-strictly positive position
In the HoTT book §5.6 ‘The general syntax of inductive definitions’ there is a proof that the existence of an inductive type $T$ with a constructor $t : ((T \to \mathsf{Prop}) \to \mathsf{Prop}) \to T$...
- 192
6
votes
0
answers
169
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 ...
- 408
5
votes
1
answer
277
views
Simple type theory: equational axioms validated by biCartesian closed categories
In this question, we consider only type theories with no ground types and no function symbols.
I want to know whether there exists a model of simple type theory with finite products, finite coproducts,...
- 193
5
votes
0
answers
216
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 ...
- 3,693
5
votes
0
answers
225
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 ...
- 357
5
votes
1
answer
383
views
What structure do all kinds of theories, models, interpretations, proofs and all that form?
This is a question about a structure that can be used to investigate all kind of structures that can be investigated. Many years ago with Joseph Gubeladze we discussed something similar but I only ...
- 17.5k
4
votes
0
answers
105
views
What exactly is the difficulty in giving a precise definition to dependent type theories?
In this talk by fields Medalist Vladmir Voevodosky on "The meta theory of dependent type theories" dated at Feb 27, 2017, the following is said:
I start with a few words about the title. ...
- 1,269
4
votes
0
answers
78
views
Lifting adjunctions along a localisation of 2-categories
Let $\mathcal S$ be a base category and let $Fib_\mathcal S^{split}$ be the 2-category consisting of split fibrations, fibered functors which strictly preserve the splitting and vertical ...
- 775
4
votes
0
answers
97
views
Minimization of second-order unifiers
We know that first-order unification is decidable.
More generally, if there exists a unifier for a first-order unification problem, then there exists a most general unifier.
I'm interested in the ...
- 186
4
votes
0
answers
133
views
Can every true type be reached from the unit type in small steps?
We are playing a game where you start at the unit type and the goal is to reach a given true type.
You can go from your current location to another by writing down a (non-dependent) function of length ...
- 41
4
votes
0
answers
123
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}$...
- 181
3
votes
0
answers
124
views
Translating set-theoretic concepts to polymorphic type theory or beyond
I've been trying to read Coquand's "An Analysis of Girard's Paradox" lately. I've noticed that he gets a type-theoretic variant of Burali-Forti's paradox once he extends Church's system with ...
- 505
3
votes
0
answers
192
views
What is the connection between these proofs of strong normalization in $\lambda^\to$ and LK?
In Ralph Loader's lecture notes on lambda calculus (section 3.3), he states that a combinatorial proof of the SN of simply typed lambda calculus uses a technique that is "in essence that used by ...
- 1,031
3
votes
0
answers
286
views
Is there a non-constructive dependent type theory?
If I understand correctly constructivism is not the only difference between intensional Martin-Löf type theory and a first-order set theory (e.g. ZFC). Can we drop constructivism and yet have a ...
- 39
3
votes
0
answers
81
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) ...
- 225
3
votes
0
answers
112
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, ...
- 375
3
votes
0
answers
168
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 ...
- 570
3
votes
0
answers
168
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 ...
- 181
3
votes
0
answers
210
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 \...
- 1,862
2
votes
0
answers
69
views
Relation of top and bottom types given multiple universes
This is something that I haven't seen mentioned in any literature.
In a type theory (extensional, intuitionistic, Martin Lof variant), given two ordered Tarski Universes such that $U_i < U_{i+1}$, ...
- 21
2
votes
0
answers
89
views
Can this predicative kind of type-set theory reach the consistency of ${\sf Z}_2$?
Add a primitive total one place fuction symbol $\tau$, and a primitive binary relation $<$, to the language of set theory. Add the following axioms:
Extensionality: $\forall z \, (z \in x \iff z\in ...
- 9,256
2
votes
0
answers
311
views
Can we have $\sf V=HTD$? How it relates to $\sf V=HOD$?
In my search for some type-set motivated line of thought that might prove axiom of choice, I was thinking of a concept that looks like $\sf V=HOD$, but in terms of types instead of ordinals, that is ...
- 9,256
2
votes
0
answers
210
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 ...
- 317
2
votes
0
answers
160
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 ...
- 9,256
2
votes
0
answers
206
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 ...
- 243
1
vote
0
answers
28
views
Any papers on the Lambek graph-$\lambda$ calculus-adjunction and the semantics of the Hindley Milner type system?
Joachim Lambek has described an adjunction between the category of graphs and the category of positive intuitionistic calculi with iteration, see e. g. Introduction to Higher Order Categorical Logic ...
1
vote
0
answers
42
views
Is stratified sorted rendering of naive set theory equivalent to tangled type theory?
I think the most important point in stratification is to have what may be called a fixed membership type distance per variable.
What I mean is that if a variable $x_i$ occurs in a stratified formula $\...
- 9,256
1
vote
0
answers
73
views
Directly proving the extensionality principle for product types without quasi-inverses
In section 2.6 of the Univalent Foundations Project's Homotopy Type Theory book, the extensionality principle of product types is proven by showing that for all elements $a:A$, $a':A$, $b:A$, $b':A$, ...
- 2,474
1
vote
0
answers
52
views
What is the consistency strength of this addition on simple type-set theory?
Language: multi-sorted first order logic with equality and membership, where for each natural $n$ there is a set $x^n$ of sort $n$. Equality "$=$" only occurs between variables of the same ...
- 9,256
1
vote
0
answers
123
views
What is the proof theoretic ordinal of this kind of predicative type-set theory?
The following is a kind of Predicative Type Set Theory.
The question is about what is exactly the proof theoretic ordinal of this theory? Is it lower than the one expected for predicative theories, i....
- 9,256
1
vote
0
answers
109
views
Can this type theory interpret second order arithmetic?
Language: multi-sorted first order logic with equality and membership, where for each natural $t$ there is a set $x^t$ of sort $t$. Equality "$=$" only occurs between variables of the same ...
- 9,256
1
vote
0
answers
232
views
Understanding the double negation modality under the "propositions as types" paradigm
$\DeclareMathOperator\Hom{Hom}$I'm trying to understand the double negation modality under the "propositions as types" paradigm, but I'm running into an apparent contradiction: let $T$ be a ...
1
vote
0
answers
198
views
What is the proof theoretic strength of PCF?
Godel's system $T$ means different, although equivalent, things to different people. To people working in the traditon of mathematical logic, $T$ is a quantifier-free equational theory of arithmetic ...
- 482
1
vote
0
answers
94
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 ...
- 11.7k
0
votes
0
answers
48
views
Product types: algebraic structure for modeling product types with commutative and associative product operation
Is there a known algebraic structure over set of Types (however they are defined) which is equipped with:
commutative and associative product operation for building product types from simpler types, ...
- 1
0
votes
0
answers
283
views
Can ∞-category be defined in proof assistants?
Can ∞-category be defined in proof assistants?
For example, we can directly consider a function such as ...
- 335
0
votes
0
answers
213
views
Is there a foundational approach that takes "structure" as primitive?
As per the title, I'd be curious to know if there have been attempts at constructing a foundation of mathematics taking, somehow, purely the notion of "structure" as primitive, maybe via a system of ...
- 22.7k