Questions tagged [type-theory]
The type-theory tag has no usage guidance.
201
questions
6
votes
1
answer
256
views
Is univalence equivalent to every type function being a functor over equivalence?
Introduce a rule in type theory that if $\Gamma \vdash f : \text{Type} \to \text{Type}$ and $\Gamma \vdash e : A \simeq B$ then $\Gamma \vdash f[e] : f(A) \simeq f(B)$.
It may seem like such a rule is ...
14
votes
1
answer
481
views
How exactly are realizability and the Curry-Howard correspondence related?
Consider, on the one hand:
the Curry-Howard correspondence between, on the one hand, types and terms (programs) in various flavors of typed $\lambda$-calculus, and on the other, propositions and ...
2
votes
1
answer
121
views
Does substitution on named terms correspond to substitution on de Bruijn terms?
Altenkirch wrote (in the unpublished draft α-conversion is easy):
I leave it to the reader to show that (some natural translation function) preserves substitution, i.e. it maps substitutions on named ...
2
votes
0
answers
67
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}$, ...
1
vote
1
answer
51
views
Constructing set-truncations of types from universes
This is a follow-up question from my previous question titled Constructing coproduct types and boolean types from universes, where I showed how every basic operation in set theory/topos theory could ...
4
votes
1
answer
140
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 ...
3
votes
1
answer
85
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 ...
6
votes
1
answer
276
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. ...
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 ...
6
votes
1
answer
231
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 ...
6
votes
1
answer
174
views
Consistency in pure type systems
Summary
My question is about how (i) a certain presentation of pure type systems in the $\lambda$-cube, bears on (ii) a standard definition of consistency in pure type systems. In short, I'm ...
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, ...
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 ...
12
votes
2
answers
800
views
An overview of mathematical-logical approaches in formalizing natural languages
Crossposted on Mathematics SE
I am an undergraduate mathematics student with a keen interest in pursuing research in the formalization of natural languages (from a more mathematical-logical approach),...
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. ...
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 ...
10
votes
2
answers
944
views
Dependent sum/product and the base-change functor adjunctions
In type theory, the dependent sum $\sum_{x : A} T(x)$ and the dependent product $\prod_{x:A} T(x)$ are defined by their introduction/elimination rules.
In category theory, we use a base-change functor....
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 ...
7
votes
1
answer
321
views
Does type theory help us avoid the "defining postulate"?
As a personal project, I decided to prove everything I learned in mathematics using formal proofs. The difference between informal proof, which is commonly used by mathematicians, and formal proof is ...
5
votes
1
answer
348
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 "...
6
votes
0
answers
274
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 ...
7
votes
1
answer
406
views
The idempotence of Mike Shulman's "Stack semantics"
I am struggling to understand lemma 7.20 of the paper Stack Semantics and the Comparison of Material and Structural Set Theories by Mike Shulman (arXiv:1004.3802). It contains formal sequents of the ...
5
votes
1
answer
157
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 ...
5
votes
1
answer
276
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,...
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 $\...
10
votes
0
answers
305
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,...
7
votes
0
answers
233
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 ...
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
votes
1
answer
322
views
Undecidable statements in type theory
In type theory, proving a statement means to exhibit an instance/element of a type corresponding to the statement. But if the statement is undecidable, no element of the type A nor its negation A → ⊥ ...
7
votes
1
answer
641
views
Open problems in type theory
I am only a beginner in the field of type theory, and I'm wondering if the community could point me out a few open problems in the field. I have a good background in logic, in particular, proof theory ...
6
votes
1
answer
142
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
votes
1
answer
393
views
Path types and identity types in dependent type theory
There's been some debate at the nLab recently over the names of "identity type" and "path type" in certain dependent type theories.
One user wrote that
Many cubical type theorists ...
4
votes
1
answer
175
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,...
-1
votes
1
answer
172
views
Is there an obvious inconsistency with this extension of Tangled Type Theory?
This posting is a follow up of this
Language multi-sorted FOL, with sorts (types) indexed by the naturals, equality symbol restricted to same type, while membership symbol restricted from lower to ...
3
votes
2
answers
492
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 ...
2
votes
1
answer
482
views
Higher inductive types in higher observational type theory
Mike Shulman gave the following set of talks on higher observational type theory earlier this year (part 1, part 2, part 3). However, while he talked about how the identity types are defined and ...
0
votes
1
answer
277
views
Is this theory equivalent to Tangled Type Theory?
Language: Multi-sorted first order logic with equality and membership, where for each natural $n$ we have variables $x_i^n$ of sort $n$, and for each decidable monotonic strictly increasing sequence ...
1
vote
0
answers
51
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 ...
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....
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 ...
0
votes
1
answer
204
views
Construct higher inductive types with only generalized algebraic data types and non-truncated quotients?
Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just ...
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 ...
6
votes
1
answer
340
views
Are infinitary monads monadic?
As discussed here, Are monads monadic?, in "On the monadicity of finitary monads" by Steve Lack, the following is shown, the forgetful functor from $Mnd_f(C) \rightarrow Endo_f(C)$ is ...
4
votes
1
answer
301
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 ...
1
vote
0
answers
231
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 ...
2
votes
1
answer
224
views
Well-behaved monad quotients
Reading through Modular specification of monads through higher-order presentations, this paper includes the following lemma within set-truncated homotopy type theory:
Given a monad $R$ (they work on ...
1
vote
0
answers
125
views
What does "sup" mean in the context of a w type? [closed]
Like the constructor for a W type is called "sup" but I don't know what that expands to. Is it super? maybe supremum? Or is it just an arbitrary name, like dynamic programming?
4
votes
4
answers
722
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)$...
6
votes
0
answers
328
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 &...
3
votes
0
answers
123
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 ...