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

learn more… | top users | synonyms

69
votes
8answers
14k 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
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 ...
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 ...
18
votes
3answers
861 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 ...
17
votes
2answers
468 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. ...
14
votes
1answer
627 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 ...
13
votes
2answers
720 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 than ...
13
votes
1answer
758 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 ...
12
votes
1answer
414 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 ...
12
votes
2answers
373 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
3answers
736 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. ...
11
votes
2answers
566 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
211 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 $\sigma\...
10
votes
4answers
355 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
615 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
781 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
397 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
165 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 ...
8
votes
1answer
150 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 x....
8
votes
1answer
411 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 ...
7
votes
1answer
536 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 ...
7
votes
2answers
350 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 ...
7
votes
1answer
95 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 ...
7
votes
0answers
90 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
3answers
294 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
2answers
266 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 ...
6
votes
1answer
68 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
2answers
76 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 ...
6
votes
1answer
221 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 ...
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
254 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
90 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
2answers
303 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
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
316 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
81 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
226 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
85 views

Formal systems in which $\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$ is true, but the contrapositive is disallowed.

Question. Are there any formal systems out there for which $$\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$$ is true, but the contrapositive $$\forall x \in \mathbb{R}(x^{-1} =...
5
votes
2answers
196 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
103 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
1answer
90 views

Categorical semantics explained – what is an interpretation?

I’ve been really having a hard time trying to understand categorical semantics. In fact, I am confused to the point I am afraid I don't know how to ask this question! I’ve been reading textbooks like ...
5
votes
0answers
185 views

What is the likely future of Univalent Foundations?

Univalent foundations has been hyped up as the foundation for mathematics for the future in articles such as this one. Now I've given HoTT a brief look, and at least seen that it appears on the face ...
5
votes
0answers
70 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} = \mathtt{...
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
144 views

Constructing a HoTT proof term of 1≠0

As an exercise in HoTT basics, I am trying to construct a term that has the type $Id_{Nat}(S(O),O)\to\bot$. If this were a Coq proof, I'd be done after a single ...
4
votes
1answer
94 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
104 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
104 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 ...