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

65
votes
8answers
13k 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 ...
21
votes
2answers
3k 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 ...
19
votes
3answers
2k 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 ...
18
votes
3answers
831 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
2answers
436 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. ...
13
votes
1answer
753 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 ...
13
votes
1answer
584 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
2answers
658 views

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

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 ...
12
votes
2answers
370 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
1answer
395 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 ...
11
votes
2answers
559 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
0answers
209 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
3answers
704 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. ...
9
votes
4answers
349 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 ...
9
votes
1answer
596 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 ...
9
votes
2answers
757 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 ...
8
votes
3answers
383 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 ...
8
votes
1answer
149 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
1answer
156 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 ...
7
votes
1answer
395 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
246 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
67 views

Let $T$ be the set of full binary trees. In what way $T^7 \cong T$?

I was reading the slides of a talk by Tom Leinster. I have trouble understanding the last line of page 17 (pages 1-15 are irrelevant and can be skipped). Could someone please explain it to me? If I ...
6
votes
1answer
479 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
2answers
304 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 ...
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
252 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
84 views

Turning ZFC into a free typed algebra

The standard way of using ZFC to encode the rest of mathematics is sometimes criticized because it introduces unnecessary, strange properties such as, for example $1\in 2$ if we encode integers by ...
6
votes
0answers
59 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
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\\ ...
5
votes
2answers
293 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
303 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
2answers
259 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 ...
5
votes
2answers
69 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
3answers
73 views

Type theory from ground up, first book recomendation

Basically I have a huge problem in finding a decent resource for learning type theory. I would like you to recommend any kind of resource for learning type theory in mathematical sense. Also I want ...
5
votes
1answer
225 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
179 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 ...
5
votes
2answers
96 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
213 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
94 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
78 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
69 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} = ...
5
votes
0answers
145 views

W-types and inverse image functor [closed]

Since the question did not get an answer here I have posted it to mathoverflow at http://mathoverflow.net/questions/218855/w-types-and-inverse-image-functor All sheaf topoi have W-types and in fact ...
4
votes
1answer
93 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
3k 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 ...
4
votes
1answer
83 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
1answer
100 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
3answers
162 views

What exactly are the numbers we use everyday?

Pi can be defined as diameter / circunference of a circle. But what is a circle? You can't tell a computer: "build a circle and divide its diameter by its ...
4
votes
1answer
66 views

The sections of the projection $\bigsqcup_{i:I} X_i \rightarrow I.$

I just noticed something funky. Let $X$ denote an $I$-indexed family of sets. There is a projection $$\pi_X: \bigsqcup_{i:I} X_i \rightarrow I.$$ It isn't necessarily surjective, of course, because ...
4
votes
1answer
91 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
3answers
173 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 ...