# Questions tagged [type-theory]

The type-theory tag has no usage guidance.

172
questions

-10
votes

0
answers

239
views

### Is there a simple example of why homotopy type theory is useful? [closed]

Feynman said that when he was attempting to understand a complex physical theory he would hold in his mind the simplest physical example to which it would apply.
This is why he was able to demolish ...

2
votes

1
answer

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

3
votes

0
answers

74
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

149
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

419
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

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

1
vote

1
answer

247
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

36
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

108
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

97
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

123
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

84
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

2
answers

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

3
votes

1
answer

143
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

131
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

191
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

103
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

469
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

237
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

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

12
votes

1
answer

528
views

### Why does Coq restrict Inductive definitions, and how is this related to Inaccessible cardinals?

Coq lets you define an inductive type of the following form:
Inductive Foo :=
| Base : Foo
| Positive : (nat -> Foo) -> Foo.
because the position of <...

24
votes

1
answer

1k
views

### Coinduction for all?

Every undergraduate in mathematics learns about proofs by mathematical induction. Moreover, every undergraduate taking a course in theoretical computer science or logic learns about inductive ...

8
votes

1
answer

449
views

### What is the status of Jordan's theorem in constructive mathematics in the language of locales?

By constructive mathematics in this matter we mean intuitionistic ZF (*).
In the language of locales, the Jordan curve can be defined as $f\colon S^1 \to X$ such that "if $U \cap V = \varnothing$,...

2
votes

1
answer

268
views

### Abstraction logic

As part of my research on building an interactive theorem proving system, I have discovered a new logic that I call Abstraction logic. I have written up the details here: https://doi.org/10.47757/...

4
votes

0
answers

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

4
votes

0
answers

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

10
votes

1
answer

918
views

### Why are W-types called "W"?

Why are W-types called "W"?
Probably "W" means either "wellordered" or "wellfounded". (Martin-Löf uses the term "wellorder".) But these are notions ...

6
votes

1
answer

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

0
votes

0
answers

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

4
votes

1
answer

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

3
votes

0
answers

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

8
votes

1
answer

600
views

### Practical Benefits of HTT/univalent foundations for assisted proofs

I'm trying to understand what the claimed practical benefits of HTT/univalent foundations are for doing computer assisted proofs and while I've seen a lot of claims of benefits they all seem to be ...

6
votes

1
answer

251
views

### Criterion for the consistency of pure type systems

Pure type systems are characterized in an almost combinatorial way: a set of axioms $\star_i : \star_j$, and a set of triples $(\star_i, \star_j, \star_k)$ saying when the dependent product $\prod_{x :...

4
votes

1
answer

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

7
votes

0
answers

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

13
votes

1
answer

460
views

### What is meant by a computational interpretation of univalence?

In homotopy type theory the univalence axiom implies function extensionality.
Suppose we have a recursive set we are not sure is empty (e.g. the set of even integers$\geq 4$ that are not a sum of two ...

2
votes

0
answers

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

7
votes

1
answer

264
views

### Categorical semantics of universe levels in dependent type theory

I know that locally closed cartesian categories provide categorical semantics for type theories with dependent products.
What kind of categories model type theories with infinite universe hierarchies (...

1
vote

0
answers

140
views

### The difference between Agda and Idris for programming using Homotopy type theory [closed]

Which is better for programming benifiting by Homotopy type theory(HoTT),Idris or Agda.compare them.

3
votes

0
answers

249
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
vote

0
answers

64
views

### Filtered colimits in type theory

My question is, what is a type theoretic way of expressing filtered colimits?
Suppose, for instance, that we would like to express the filtered colimit of objects in a dependent type theory. How might ...

1
vote

0
answers

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

1
vote

0
answers

146
views

### constructive type theory references books

What is the best book you recommend for a beginner in constructive type theory applied to computer science?

33
votes

3
answers

4k
views

### Top-down mathematics, or "Where it all begins"

Sorry if this is off-topic.
It was my attempt to take a top-down approach to mathematics.
Being an inexperienced undergraduate (so please take my writing here lightly), I've been presented with ZFC as ...

6
votes

2
answers

330
views

### Characterization of 'canonical' natural numbers objects

Canonicity is a useful property satisfied by some type theories, saying that every element of natural number type is propositional equal to an element of the form $s^n(0)$, where $s$ is the successor ...

7
votes

1
answer

270
views

### Ordered logic is the internal language of which class of categories?

Wikipedia says:
The internal language of closed symmetric monoidal categories is linear logic and the type system is the linear type system.
"A Fibrational Framework for Substructural and Modal ...

7
votes

2
answers

276
views

### Explicit different proofs of the same identity type in MLTT

This question is similar to (but more specific than) this one: When are two proofs of the same theorem really different proofs
I do not know very much about homotopy type theory, but I am trying to ...

11
votes

1
answer

539
views

### 3 questions about basics of Martin-Löf type theory

I started to read the HoTT book. I'm now on chapter 1 and I have several questions concerning not even homotopical, but "regular" type theory.
On page 24, where the universes are introduced,...

3
votes

0
answers

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

17
votes

2
answers

786
views

### Are we sure the calculus of inductive constructions and ZFC plus countably many inaccessible cardinals are equiconsistent?

This answer says,
IIRC, the calculus of inductive constructions is equi-interpretable with ZFC plus countably many inaccessibles — see Benjamin Werner's "Sets in types, types in sets". (...