# Questions tagged [type-theory]

For questions about type theory, including normalization, dependent types, identity types, inductive types, universe types, functional programming languages, proofs as programs in simply-typed lambda-calculi, Martin-Löf's intuitionistic type theory or related.Consider using one of the following tags: (lambda-calculus), (logic), (constructive-mathematics),(homotopy-type-theory) if related.

338 questions
25 views

35 views

### What is the name of a coinductive type defined with a total order relation?

In type theory, is there a name for a coinductive type simply defined with a successor operator and an equivalence relation? And what would be the name of such a type if it were defined with a total ...
37 views

### Type equivalence in $\lambda\underline\omega$ under lambda abstraction

I'm going through "Type Theory and Formal Proof" by Nederpelt and Geuvers and just trying to play around with $\lambda\underline\omega$ after reading the chapter on it to better grasp the material. ...
62 views

### Properties over partly specified inductive families (HoTT)

At the moment I'm about to get my head around homotopy type theory as a new perspective into mathematics. Insofar, I'm trying to mess around with it, prove some simple things and see where it gets; ...
139 views

### Intuition for Diaconescu's theorem

Diaconescu's theorem proves that the axiom of choice implies the law of the excluded middle. While I can follow the proof in the above wikipedia article, it just seems like a cheap trick, so to ...
50 views

### Prospects of teaching/learning elementary math with computed-checked type theory

I've read as much as I can understand about type theory and homotopy type theory (HoTT) and it seems like these are very promising directions for re-foundationalizing mathematics in a way where ...
110 views

### What would synthetic linear algebra look like?

I'm aware of synthetic mathematical fields like synthetic differential geometry and synthetic topology where the area is developed axiomatically rather than deriving everything analytically from a ...
44 views

### Universal quantifiers in category theory

I’ve recently learned about the curry howard isomorphism for dependent type theory, and I’m now interested in learning about how to capture this in category theory. I believe that I understand how to ...
34 views

### Introduction to categorical logic and CHL-correspondence?

My motivation for this question is that I’m interested in using categorical logic/category theory to intuitively visualize and think about proofs in advanced type-theory based proof-assistants like ...
88 views

### Different descriptions of internal languages of a topos

I wanted to learn more about the internal language of of toposes and to do so I have been reading both Sheaves in Geometry and Logic (Sheaves) by Mac Lane and Moerdijk and Introduction to Higher Order ...
61 views

### Model for the type-theoretic axiom of choice in Coq.

This is the request for references. It is a known fact that there is a model of ZFC in ZF, so ZFC is consistent if ZF is consistent. It is also know that there is a double-negation Godel-Gentzen ...
67 views

### Products are to Cartesian multicategories as exponentials are to what?

Section 2 of this draft by Mike Shulman explains how Cartesian multicategories are able to directly internalize the structural rules of simple intuitionistic type theory as it is usually presented, ...
287 views

### Can the axiom of choice be explicitly proved in (intuitionistic) predicate logic, or is something like intuitionistic type theory necessary?

In intuitionistic mathematics, an axiom of choice of the form $$\forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x, fx)$$ is valid by the meaning of the quantifiers (comp. Dummett, ...
84 views

### Questions on the “free functor” functor

I have recently found out that in Haskell we can to turn a type constructor into a functor, using the "free functor" construction [1, 2, 3]. I would like to understand this construction – the free ...
32 views

### Closure of a constant

Consider a type $T$, and a set $S$ containing elements of type $T$. An object $f$ of type $T→T→T$ (or $T^2 → T$) is a function and it is closed under $S$ if any two elements of $S$ applied to $f$ ...
99 views

### Examples of the categorical interpretation of dependent types

I'm trying to understand the correspondence between dependent types and category theory. Let me tell you about my current (I admit, limited) knowledge on the two topics.....
206 views

### Is many sorted logic really a unifying logic?

I am reading "Extensions of First Order Logic" by Maria Manzano (1996). It develops the thesis that "[M]ost reasonable logical systems can be naturally translated into many-sorted first order ...
91 views

### Can we prove that the peano axioms are true for $(\mathbb N, \sigma)$ in type theory?

In mathematical logic that I'm used to (i.e. we have first-order formulas and a sequent calculus to derive formula's from axioms), we never prove that the peano axioms are true for the natural numbers,...
63 views

### The continuation passing style transformation in the lambda calculus

I have an issue understanding the following definition (from https://tel.archives-ouvertes.fr/tel-00783245/document , p.82) of the continuation-passing style (CPS) transformation in the lambda ...
52 views

### definitional extension vs. $\lambda$-abstraction
Let $\mathcal{L}$ be a first-order language in signature $\Sigma$ and $\mathcal{L^+}$ an extension of $\mathcal{L}$ in a richer signature $\Sigma^+$. An $\mathcal{L^+}$-theory $T^+$ is a definitional ...
As I understand the Liskov Substitution Principle, it says that if $A\subset B$ and $X \subset Y$ then $(B\to X) \subset (A\to Y)$. I'm having trouble understanding what the converse of this ...