Questions tagged [type-theory]
The type-theory tag has no usage guidance.
200
questions
6
votes
1
answer
280
views
In HoTT with LEM, are sets and pointed sets the same thing?
The operations of adding and removing a point (where removing is a consideration of a subset of elements x such that $(x = *) \to 0$) implements the equivalence of these 1-types, as far as I can see. ...
- 6,484
6
votes
1
answer
236
views
Existence property for second-order propositional logic
Consider the intuitionistic second-order propositional calculus (SOL) formulated in the full $\wedge,\vee,\rightarrow,\bot,\top,\forall,\exists$ language.
Question: Assume that $\Gamma$ and $\Psi$ are ...
- 606
6
votes
2
answers
694
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 $\...
- 469
6
votes
1
answer
679
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 ...
- 2,283
6
votes
1
answer
323
views
Does simple theory of types + ambiguity prove axiom of infinity?
Does simple theory of types + ambiguity prove axiom of infinity?
The simple theory of types known as $\sf TST$ is a multi-sorted first order theory, syntactical restrictions include $\in$ being a ...
- 9,266
6
votes
1
answer
146
views
Univalence for weakly Tarski universes
In Martin-Löf type theory, a weakly Tarski universe is a type $\mathcal{U}$ with a type family $\mathcal{T}(A)$ indexed by terms $A:\mathcal{U}$, which is closed under identity types, dependent ...
- 2,474
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.6k
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
394
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 ...
- 3,693
5
votes
1
answer
729
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 ...
- 53
5
votes
1
answer
162
views
Are lists in homotopy type theory free $A_\infty$-spaces?
Traditionally in dependent type theory with axiom K or uniqueness of identity proofs, every type $A$ is 0-truncated, and thus the type of lists on $A$, $\mathrm{List}(A)$, is 0-truncated and the free ...
- 2,474
5
votes
2
answers
685
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....
- 51
5
votes
1
answer
354
views
Book that shows a construction of ZFC with Calculus of Constructions
Is there any book that teaches the basics of Type Theory and Calculus of Inductive Constructions (CIC) and also shows a construction of ZFC (or preferably NBG) in CIC?
I only found the paper "...
- 483
5
votes
1
answer
164
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 "...
- 40.2k
5
votes
1
answer
896
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 ...
- 369
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
4
answers
739
views
Why in Martin-Löf type theory any natural number is assumed to be either $0$ or $S(a)$ for some $a\in\mathsf{N}$?
In laying down the equality rules in Martin-Löf type theory, e.g., for the type $\mathsf{N}$ of natural numbers, there seems to be an implicit assumption that any natural number is either $0$ or $S(a)$...
- 505
4
votes
3
answers
599
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 ...
- 233
4
votes
1
answer
429
views
In cubical type theory, can we insist that "constant" compositions are the identity?
$\DeclareMathOperator{\comp}{comp}\DeclareMathOperator{\refl}{refl}\DeclareMathOperator{\transp}{transp}$I've been reading about Cubical Type Theory and playing around with the Agda implementation of ...
- 580
4
votes
1
answer
501
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 ...
- 143
4
votes
3
answers
357
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 ...
- 2,775
4
votes
1
answer
146
views
Constructing coproduct types and boolean types from universes
Suppose we have a dependent type theory which has dependent product types, dependent sum types, identity types, function extensionality, an empty type, and a universe $U$ which is closed under the ...
- 2,474
4
votes
1
answer
453
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.
- 43
4
votes
1
answer
176
views
Extending the class of primitive recursive functions with higher order recursion schema
I'm trying to extend the class of primitive recursive functions by extending the recursion schema over higher types.
We usually define the class of primitive recursive functions by using zero function,...
- 301
4
votes
1
answer
304
views
Codependent types in type theory
The nLab's article on coinductive types here states that
There is an obstacle to the complete dualization of the usual rules for inductive types in homotopy type theory, including dualizing the ...
- 2,474
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
2
answers
493
views
Can we write Tangled Type Theory without reference to type sequences?
I just want to know if Tangled Type Theory $\mathsf{TTT}$ of Randall Holmes ([see: Holmes - NF is consistent, p:11, Holmes - The equivalence of NF-style set theories with “tangled” type theories; the ...
- 9,266
3
votes
1
answer
297
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 ...
- 585
3
votes
2
answers
537
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 ...
- 165
3
votes
2
answers
572
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 ...
- 4,353
3
votes
1
answer
287
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\...
- 85
3
votes
1
answer
246
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 \...
- 365
3
votes
1
answer
128
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,299
3
votes
1
answer
90
views
How to represent morphisms in a fibration in the internal type theory
Given a fibration $p:\mathcal{E \to B}$, we can work with a minimal type theory with semantics in $p:\mathcal{E \to B}$, its internal type theory.
The type theory for $p$ is dependent, with contexts ...
- 1,043
3
votes
1
answer
658
views
Data abstraction in set theory via Urelements
I am working in a setting of set theory where set theory is embedded in simply-typed higher-order logic, basically as described for example in
Chad E. Brown and Cezary Kaliszyk and Karol Pak (2019) ...
- 179
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
269
views
Intuitive (topological) explanation of a proof from the HoTT book [closed]
My friends and I are struggling with understanding intuitively the proof of equivalence between based and free path inductions (HoTT book 1.12.2)
The first major problem is understanding the meaning ...
- 1,294
3
votes
0
answers
287
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
276
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 ...
- 31
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