# Questions tagged [type-theory]

The type-theory tag has no usage guidance.

**2**

votes

**0**answers

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

**11**

votes

**2**answers

831 views

### What does “simplification of proofs as evaluation of programs” mean?

I am currently going through Philip Walder's "Proposition as Types" and a passage of the introduction has struck me:
for each way to simplify a proof
there is a corresponding way to evaluate a ...

**4**

votes

**0**answers

115 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}$...

**7**

votes

**1**answer

468 views

### Constructing unnatural transformations

In a nutshell, the question is: is it true that any explicit (not involving axiom of choice) pointwise transformation between sufficiently complicated functors is natural almost everywhere?
Let $C$ ...

**32**

votes

**1**answer

4k views

### Homotopy Type Theory: What is it?

My question is, broadly, what is the main project of Homotopy Type Theory (HoTT). I asked a professor who is likely to be correct and he say the following:
There are three directions:
...

**3**

votes

**0**answers

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

**6**

votes

**0**answers

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

**7**

votes

**3**answers

593 views

### Extensionality in HoTT versus extensionality in internal language of a category

What's the extension of judgmental identity in HoTT (homotopy type theory)?
The Martin-Löf intensional dependent type theory with identity types is called (definitionally) extensional if the ...

**5**

votes

**2**answers

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

**9**

votes

**2**answers

543 views

### How should I be thinking about object classifiers / universal fibrations / universes?

I have been learning about homotopy type theory this summer. I am not a homotopy theorist but I am more comfortable with homotopy theory than I am with type theory, so the way I rationalize many of ...

**13**

votes

**3**answers

668 views

### Formal/rigorous treatment of (im)predicativity/predicativism

There are several places on the web where one may find quite intuitively understandable accounts of (im)predicativity; here on MO I found two questions with very good detailed answers (Predicative ...

**3**

votes

**1**answer

236 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\...

**11**

votes

**2**answers

2k views

### Why is there no product type in simply typed lambda-calculus?

Consider simply typed $\lambda$-calculus that has only the unit type as primitive. We would like to encode the product and the sum types. An encoding of the product type in the untyped $\lambda$-...

**4**

votes

**2**answers

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

**13**

votes

**2**answers

1k views

### What is the status of (universal) algebra in type theory?

With the recent interest in homotopy type theory as a foundation for mathematics, it seems natural to develop algebra within the framework of type theory. So far, I can't find much literature ...

**0**

votes

**1**answer

248 views

### Does “Church's Law” really fail in Extensional Type Theory?

Last year Bob Harper wrote a blog post about the failure of "Church's Law" in Extensional Type Theory[1]. However his statement of the law looks to me more like an internal version of the statement "...

**7**

votes

**1**answer

471 views

### The independence of path induction

In §1.12 of the Homotopy type theory book, it is mentioned that indiscernibility of identicals is a consequence of path induction. More precisely, for each type $C$ dependent over a type $A$, there is ...

**9**

votes

**2**answers

1k views

### A (very naive) question about Homotopy Type Theory

In homotopy type theory, homotopy types can be viewed as logical types and it is possible to prove some theorems about them without using any underlying space (no simplicial set, no topological space)....

**16**

votes

**2**answers

999 views

### $\infty$-categorical interpretation of type theory

One can read at several places that Martin-löf type theory should be the internal language of a locally Cartesian closed infinity category, and that the univalence axiom should distinguished infinity ...

**20**

votes

**2**answers

2k views

### Prospects for reverse mathematics in Homotopy Type Theory

Reverse mathematics, as I mean here, is the study of which theorems/axioms can be used to prove other theorems/axioms over a weak base theory. Examples include
Subsystems of Second Order Arithmetic (...

**6**

votes

**1**answer

366 views

### $\Pi$, $\Sigma$, and identity types without $\eta$ in comprehension categories

In comprehension categories, dependent sums are defined as a choice of left adjoints for all reindexing functors along display maps, satisfying a Beck-Chevalley condition. Dependent products are ...

**7**

votes

**0**answers

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

**11**

votes

**3**answers

1k views

### Equivalent form of the Univalence Axiom

I'm reading the new HoTT book and I'm wondering about a potential equivalent form of the Univalence Axiom: $(A \simeq B) \simeq (A = B)$.
For simplicity, I'm tacitly working in a fixed universe. It ...

**18**

votes

**3**answers

1k views

### How do we express measurable spaces using type theory?

A measurable space $(X,\mathcal X)$ consists of a set $X$ equipped with a $\sigma$-algebra of subsets $\mathcal X$. I would like to write computer programs involving measurable spaces, but to the best ...

**8**

votes

**2**answers

966 views

### Connection between codata and greatest fixed points

This is, I'm afraid, another question that MSE couldn't answer.
It's easy to see how inductively-defined data types correspond to least fixed points. Let's take the natural numbers as an example, ...

**14**

votes

**1**answer

2k views

### Forcing in Homotopy Type Theory

I apologize if this question doesn't make any sense. I'll just go ahead and delete it if that's the case. But the question is just the title. Is there a notion of forcing in homotopy type theory? ...

**0**

votes

**1**answer

451 views

### prod and sig in COQ

Hello,
Apparently in COQ the type prod (with one constructor pair) corresponds to cartesian product and the type sig (with one constructor exist) to dependent sum but how is described the fact that ...

**2**

votes

**1**answer

185 views

### Is there research on the notion of co-accessibility?

I want to start off with a disclaimer that I am only a mathematical amateur. Please forgive me for ignorance or any non-standard nomenclature I use here :)
Let's start off with some context.
Let X ...

**1**

vote

**0**answers

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

**9**

votes

**2**answers

661 views

### Category of Judgements?

I have been able to find a lot of information on the category of contexts -- for example, the page on syntactic categories at the nLab is a good starting point. However, when I try to find similar ...

**6**

votes

**1**answer

1k views

### intensional equality in type theory

I want to know why we add an intensional equality in type theory to definitional equality ?
What is the aim with this intensional equality ?
thanks

**6**

votes

**2**answers

305 views

### Why no morphisms from the contradictory proposition to the inconsistent context?

Consider Higher order predicate logic over dependent type theory (DPL) as defined in Chapter 11 of B. Jacobs's book "Categorical Logic and Type Theory" (though I think this question applies to first-...

**9**

votes

**2**answers

327 views

### Categorical semantics of W-types

Jacob's book titled "Categorical Logic and Type Theory" gives a nice description of Π and Σ types as adjunctions to substitution functors induced by display maps. Is there a similar ...

**8**

votes

**2**answers

413 views

### Reduction rules for inductive types

(I'm not sure if I should post this here rather than at Theoretical Computer Science, I've found a lot of type theory related questions on MathOverflow)
I'm working in Martin-Löf type theory with ...

**4**

votes

**1**answer

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

**15**

votes

**3**answers

4k views

### What is the theory of polynomials?

We all know what polynomials are, along with their elementary properties and many effective algorithms for different representations of polynomials.
The question here is more of a universal algebra ...

**7**

votes

**1**answer

1k views

### categorifying induction in homotopy type theory

In trying to understand homotopy type theory, I stumbled upon the following silly question, which is likely to be trivial for the experts.
Let $B=\sqcup_{n\in\Bbb N} BS_n$, which I'd like to think of ...

**19**

votes

**3**answers

1k views

### Surreal Numbers as Inductive Type?

Prompted by James Propp's recent question about surreal numbers, I was wondering whether anyone had investigated the idea of describing surreal numbers (as ordered class) in terms of a universal ...

**43**

votes

**7**answers

8k views

### How true are theorems proved by Coq?

Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one makes with respect to ...

**6**

votes

**1**answer

956 views

### What fails when using call/cc as realizer of the Peirce formula

Define the axiom constants $p_{A,B}^{((A\rightarrow B)\rightarrow A)\rightarrow A}$ as realizers of the Peirce formula, and $f_A^{\bot\rightarrow A}$ as realizers of the Ex Falso Quodlibet. Then $p_{A\...

**-1**

votes

**5**answers

843 views

### finding cutting edge papers and books

Hi all,
what are the best strategies to find cutting edge papers and books on a field of mathematics?
..
Example:
2-3 years ago I had to analyze a time series. I found a paper and showed that to ...

**8**

votes

**3**answers

730 views

### What do I call type theory without Curry-Howard?

Is there a word I can say which will convey to type theorists that I am not thinking about types as propositions?
Background: as a category theorist, I am mostly interested in type theories as a ...

**4**

votes

**3**answers

587 views

### Can a typing judgment admit essentially different derivations?

In any sort of type theory, there are a bunch of rules for constructing derivations of typing judgments such as $x:A,\; y:B(x) \;\vdash\; z:C(x,y)$. (I intend to include also judgments of the form $B:...

**3**

votes

**0**answers

201 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 \...

**2**

votes

**1**answer

254 views

### Relation between different definitions of types [closed]

Is there any connection between the definition of type in model theory and the definitions from type theory? Is there any explanation why the same term is used for these notions, maybe in the ...

**6**

votes

**4**answers

830 views

### What is the intuitive meaning of star and box in a pure type system?

The systems of the λ-cube have the axiom $\star:\square$.
I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meanings of $\star$ and $\...

**2**

votes

**2**answers

1k views

### What is a semigroup or, what do I do with that associativity proof?

Mathematically, I know what a semigroup is: It is a set S along with an associative binary operation $* : S \times S \rightarrow S$. So far, so good.
From a computational perspective, one can ...

**13**

votes

**4**answers

1k views

### Reference request for type theory

I am interested in learning the theory of types, especially in how they can provide a foundation to mathematics different to sets and how they can avoid self-referential paradoxes by stipulating that ...

**20**

votes

**2**answers

3k views

### What is the manner of inconsistency of Girard's paradox in Martin Lof type theory

I am aware that assigning the type of Type to be Type (rather than stratifying to a hierarchy of types) leads to an inconsistency. But does this inconsistency allow the construction of a well-typed ...

**9**

votes

**4**answers

1k views

### Can dependent sums be encoded as dependent products?

Please forgive any unorthodox notation or obvious errors here... I'm trying to get an intuition for dependently typed languages, so I'm starting out by seeing which analogies I can take from the ...