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

learn more… | top users | synonyms

50
votes
8answers
9k views

Learning Lambda Calculus

What are some good online/free resources (tutorials, guides, exercises, and the like) for learning Lambda Calculus? Specifically, I am interested in the following areas: Untyped lambda calculus ...
16
votes
3answers
708 views

What good is infinity?

I am becoming increasingly convinced that Wildberger's views are, if a little bizarre, at least not hopelessly inconsistent. When I was reading the comments in the video following (MF17), somebody ...
16
votes
3answers
1k views

Why is it worth spending time on type theory?

Looking around there are three candidates for "foundations of mathematics": set theory category theory type theory There is a seminal paper relating these three topics: From Sets to Types to ...
16
votes
2answers
2k views

Classic type theory textbooks

There are many classic textbooks in set and category theory (as possible foundations of mathematics), among many others Jech's, Kunen's, and Awodey's. Are there comparable classic textbooks in ...
12
votes
1answer
411 views

Type theory as foundations

Does anyone know any good references that describe type theoretical foundations of mathematics? I've read some books e.g. Winskel's The Formal Semantics of Programming Languages and Pierce's Types and ...
12
votes
1answer
345 views

Looking for an approach to mathematical notation wherein the universe is divided into disjoint worlds.

Is there a rigorous approach to mathematical notation wherein the "universe" is divided into disjoint "worlds," and the meaning of notation is world-dependent? This would solve a few pesky problems. ...
11
votes
2answers
502 views

How to introduce type theory to newcomer

I want to introduce (dependent) type theory to some friends having background in mathematical logic and set theory. To make this introduction easy I would like to give an informal presentation that ...
11
votes
1answer
707 views

If $f(x)=g(x)$ for all $x:A$, why is it not true that $\lambda x{.}f(x)=\lambda x{.}g(x)$?

There's something about lambda calculus that keeps me puzzled. Suppose we have $x:A\vdash f(x):P(x)$ and $x:A\vdash g(x):P(x)$ for some dependent type $P$ over a type $A$. Then it is not necessarily ...
11
votes
1answer
338 views

Hao Wang's $\mathfrak S$ system/$\Sigma$ system: a “transfinite type” theory that avoids the Goedel's theorems.

Long ago, while I was reading a book ($*$) about the various way to build set theories (Zermelo-Freankel, Von Neumann–Bernays–Gödel, and type theories), I read about a variant of type theory with ...
11
votes
0answers
193 views

Reference on standard types

This question is about what I presume is a basic construction in type theory. The finite types are defined as follows: 0 is a finite type; if $\sigma, \tau$ are finite types, then so is ...
10
votes
2answers
308 views

What is the best path to learn Category theory and Type thoery?

I have little background in Programming in functional languages and wanted to learn type theory. I started with taking Homotopy type theory class Online videos of Robert Harper. I thought rather ...
9
votes
1answer
319 views

Confusion about Homotopy Type Theory terminology

I've picked up the Homotopy Type Theory book for leisure. I'm comfortable with strongly typed languages and familiar with dependently typed languages and I enjoy topology, so I thought that the HoTT ...
8
votes
3answers
495 views

Introductory books as preparation to read Voevodsky homotopy-theory (HoTT) book

I would like to read Voevodsky HoTT book. However, I lack a lot of the basics. I would need a few introductory books first that cover topics like groupoids, fibrations, W -types, Homotopy theory. ...
8
votes
4answers
300 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
8
votes
1answer
504 views

Intuitionistic Banach-Tarski Paradox

While the Banach-Tarski paradox is a counter-intuitive result which requires the Axiom of Choice, leading some people to argue specifically against Choice, and others to argue for constructive ...
8
votes
1answer
140 views

How to prove that these are the only type inhabitants?

Consider a type $$\mathsf{Boolean} = \forall \alpha.\ \alpha \to \alpha \to \alpha$$ with its two inhabitants \begin{align} \mathrm{tt} &= \lambda x.\ \lambda y.\ x \\ \mathrm{ff} &= \lambda ...
7
votes
2answers
587 views

What's the meaning of algebraic data type?

I'm reading a book about Haskell, a programming language, and I came across a construct defined "algebraic data type" that looks like ...
7
votes
1answer
322 views

Axiom of Choice - Type Theory (Proof)

Background In Intuitionistic Type Theory (p. 27-28), Martin Löf provides a proof of the axiom of choice that is constructively valid. This version is considerably weaker than the ordinary set theory ...
6
votes
3answers
272 views

Does $A\times A\cong B\times B$ imply $A\cong B$?

This is similar to What does it take to divide by $2$? about $(A\sqcup A\cong B\sqcup B)\Rightarrow A\cong B$ which is valid in $\textsf{ZFC}$ by using cardinalities and also in $\textsf{ZF}$ by some ...
6
votes
3answers
122 views

Types, Sets and Categories

I am learning Category Theory and at first I just pictured a category like a class in object oriented programming: type definition + methods (morphisms). However the author I am reading uses maps ...
6
votes
1answer
325 views

Difference between a type and a set

I've been trying to understand this distinction for a while, buts its still not making sense to me. Originally, I thought the distinction between type and set was as follows. The relationship ...
6
votes
1answer
1k views

Relationship between propositional logic, first-order logic, second-order logic higher-order logic, and type theory

I understand there is propositional logic, first-order logic, second-order logic higher-order logic, and type theory, where the latter logics are extensions of the former logics. Can someone explain ...
6
votes
3answers
237 views

Peano axioms expressed in type theory

I have a very strong understanding of 1st order logic and am trying to lean type theory as an alternative. Could someone express the Peano axioms with type-theory? I am especially interested to see ...
6
votes
0answers
48 views

What is the actual significance of the lambda calculus for the formalization of math?

The Simply Typed Lambda Calculus was proposed initially as a foundational system for the formalization of mathematics. As such, I would expect that soon there would be attempts to implement most of ...
5
votes
2answers
254 views

Two questions on homotopy type theory

In reading the HoTT book, I have found that it is easy to become bogged down in detail and hard to tell the general 'big picture' of what is going on. I hope to get some general answer to the ...
5
votes
2answers
239 views

Eilenberg Moore category

I've been trying to code up the Eilenberg-Moore category for a monad in Haskell. As I understand it, given a category $C$ and a monad $(T,\eta,\mu)$ on $C$ we build the Eilenberg-Moore category $C^T$ ...
5
votes
1answer
121 views

Is there a fundamental distinction between objects and its types?

My question is related to the formal presentation of type theory as stated in the context of Homotopy Type Theory. Every formalization is grounded on typing judgements like $$ a: A $$ where mostly it ...
5
votes
2answers
192 views

Is higher order type theory the same as higher order logic?

The internal language of a topos is higher order intuitionistic type theory (or logic). Here the higher order simply refers to allowing function types. In mathematical logic we have higher-order ...
5
votes
2answers
49 views

Basic Definition of Dependent Types?

I'm looking at the wikipedia page for Dependent Types and I am getting stuck trying to understand the definition. It says, ... given a type $A:U$ in a universe of types $U$, one may have a ...
5
votes
1answer
214 views

Foundational theories, their uses, interactions and comparisons?

Until now, I heard that there are some theories for building mathematical objects (or at least it is what it seems to my poor knowledge). Some of these are: Set theory; Logic; Category theory; Type ...
5
votes
2answers
92 views

Is there a theory of extensible definitions?

We can define $+$ as a function $\mathbb{N}^2 \rightarrow \mathbb{N}$, and then prove: Theorem 1. The range of $+$ is $\mathbb{N}$. If we later wish to extend $+$ to a function $\mathbb{Z}^2 ...
5
votes
1answer
158 views

How does type theory handle division by zero and such?

Say I have a program that needs to not divide by zero: f(x): if nonzero(x): return sin(x)/x else: return 1 If we divide by zero, we get ...
5
votes
1answer
65 views

Is there a syntax for type quantification in higher order logic?

I'm trying to understand higher order logic deduction, and I sort of understand how after going to third order logic and higher you have a type explosion; predicates and functions can have a large ...
5
votes
0answers
57 views

Elementary proof of compact space = exhaustible space?

(This is a repost of a question I asked last year on cs.stackexchange.) The work of Martín Escardó has demonstrated close parallels between classical topology on one hand and computability on the ...
5
votes
0answers
59 views

Path structure of an odd-looking higher inductive type.

Consider the (putative) higher inductive type $\mathtt{PNest}$, with the constructors: $\mathtt{base} : \mathtt{PNest}$ $\mathtt{nest} : \mathtt{base} = \mathtt{base} \to \mathtt{base} = ...
4
votes
1answer
90 views

How to describe free magmas in more structuralist terms?

Given a generating set $G$ (assume for simplicitly it consists entirely of urelements), the free magma on $G$ can be described concretely as follows. Its underlying set is the least $U \supseteq G$ ...
4
votes
2answers
1k views

Curry-Howard correspondence

I read that the Curry-Howard correspondence introduces an isomorphism between typed functions and logical statements. For example, supposedly the function $$\begin{array}{l} I : \forall a. a \to a\\ ...
4
votes
1answer
50 views

What breaks the Turing Completeness of simply typed lambda calculus?

On the Wikipedia page about Turing Completeness, we can read that: Although (untyped) lambda calculus is Turing-complete, simply typed lambda calculus is not. I am curious as to what exactly ...
4
votes
2answers
233 views

How to understand the definition of sets in homotopy type theory and the role of univalence?

Bear with me, I'm a physicist. In homotopy type theory, as I understand it, a type $X$ is a set if all the morphisms over its terms $x:X$ are identies. When I say "morphisms", then I view the term as ...
4
votes
1answer
89 views

Is there such a thing as 'typed mathematics?'

In response to Is an empty set equal to another empty set?, I have another question. In 'untyped' (regular) mathematics, any two empty sets are equal. The set of invisible hats and the set of ...
4
votes
2answers
105 views

What is the difference between intuitionistic, classical, modal and linear logic?

I am currently going through Philip Walder's "Proposition as Types" and a passage of the introduction has struck me: Propositions as Types is a notion with breadth. It applies to a range of ...
4
votes
1answer
49 views

How high up do kinds go in type theory?

I understand this is a bit naive, but I just learned how types can have types that we call 'kinds,' in system F$\omega$ as a sort of extended higher order lambda calculus. The wiki article on it ...
4
votes
1answer
200 views

Logic within Type theory. Is there a rough academic consensus on how this should be done?

I guess because of it's presence in several blogs on math and even physics, I've recently started to learn some type theory, often from people who know about it and from books which use it. I want to ...
4
votes
1answer
46 views

Basic Propositional Logic

I'm working through Thompson's Type Theory and Functional Programming. I've only read the first chapter and want to make sure I'm understanding the material. The first problem asks to prove the ...
4
votes
3answers
135 views

What's a good resource to learn about the simply typed lambda calculus?

I've read An Introduction to Functional Programming Through Lambda Calculus by Greg Michaelson, and found it to be a very good resource to learn about the untyped lambda calculus. However, I want to ...
4
votes
0answers
87 views

Logic in closed symmetric monoidal categories; reference request.

Suppose we want an algebraic theory $T$ to be interpretable in any closed symmetric monoidal category $\mathbf{C}.$ I am thinking in particular of the case where $\mathbf{C}$ is the category of models ...
4
votes
1answer
137 views

Curry-Howard Correspondence (Proof Theory)

As you all know, the Curry-Howard correspondance provides a link between type theory and predicate logic. Concepts featured in the former, such as $\Pi$-type and $\Sigma$-type can, by the ...
4
votes
0answers
110 views

W-types and inverse image functor

All sheaf topoi have W-types and in fact there's an explicit construction given by Benno van den Berg & Ieke Moerdijk, but the construction is quite involved. I would like to know whether the ...
3
votes
2answers
63 views

Questions regarding well formed expressions in the Theory of types

I'm dealing with a question in type theory: Is it possible to assign types to $\alpha$, $\beta$, and $\gamma$ in such a way that both $(\alpha (\beta))(\gamma)$ and $\alpha (\beta (\gamma))$ are ...
3
votes
2answers
1k views

Constructing dependent product (right adjoint to pullback) in a locally cartesian closed category

I've been trying to find a proof that the pullback functors in a locally cartesian closed category have right adjoints (used to model the notion of indexed product inside a category (rather than ...