# Questions tagged [type-theory]

The type-theory tag has no usage guidance.

201
questions

4
votes

1
answer

237
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

458
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

120
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

49
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

134
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

83
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

267
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

224
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

172
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

47
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

780
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

166
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

910
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

314
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

337
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

271
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

400
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

41
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

304
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

228
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

611
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

141
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

373
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

173
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

171
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

487
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

468
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

273
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

108
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

197
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

295
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

225
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

221
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

123
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

703
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

321
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

122
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 ...