# Tagged Questions

The type-theory tag has no wiki summary.

6answers
2k 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 ...
1answer
468 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 ...
0answers
111 views

### Hao Wang's $\mathfrak S$ system: a “transfinite type” theory?

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 ...
2answers
335 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 ...
1answer
277 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 ...
0answers
167 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. ...
2answers
335 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 ...
2answers
63 views

### Is there a theory of extensible definitions?

We can define $+$ as a function $\mathbb{N}^2 \rightarrow \mathbb{N}$, and then prove the theorem: Thm. The range of $+$ is $\mathbb{N}$. If we later wish to extend $+$ to a function \$\mathbb{Z}^2 ...
2answers
69 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$ ...
2answers
118 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 ...
2answers
271 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\\ ...
0answers
41 views

### Are large cardinals bi-interperable with type theory?

"Sets in Types, Types in Sets" establishes that the calculus of constructions is bi-interpretable with ZFC + infinitely many inaccessibles. Are there any more results like this higher up the large ...
2answers
212 views

### Has a Dependent Type always a Type?

I am experimenting with dependent types. Lets assume the following short notation: ...
1answer
216 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 ...
0answers
60 views

### Introductory text about different stratification methods in higher-order logic and set theory

Could someone recommend me a good overview text about stratification of predicates, comprehension axioms, and other methods of avoiding the paradoxes in untyped or only loosely/relatively typed ...
2answers
243 views

### formal rules for avoiding bound/unbound variable problems in lambda calculus

I have been interested in learning formal math formally enough so that I could write a proof assistant using some simple parsing tools, and explain to someone else with little math knowledge how to ...
2answers
132 views

### Accessible formal specification and explanation of First Order Logic?

I am trying to get good at proofs by working through How To Prove It. Unfortunately I am very bothered by the fact that I do not understand all the formalities in First Order Logic + set theory ...
1answer
28 views

### Variables in Types in type theory

I'm slowly grasping this, though the different formulations of type theory make it difficult. In http://imps.mcmaster.ca/doc/seven-virtues.pdf types can only be formed from *, i, and a->b when a and ...
1answer
27 views

### in type theory does (x:A) imply ((x:A):A)

In the formulation of type theory I'm reading, (x:A) is an expression of type A. This would seem to imply ((x:A):A) and (((x:A):A):A)... Is this a common feature of type theories? Or am I reading too ...
2answers
28 views

### mapping simple first oreder problems to type theory

Since Peano axioms expressed in type theory doesn't seem to be going anywhere, here is a simpler question: How would I map simple first order systems to an equivalent type theoretic notation. ...
0answers
39 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 ...
0answers
26 views

### Enumeration of symbols in grammatical expressions or vertices in tree graphs

I have expressions (type of a function) like e.g. $$f:(A\to B)\to C \to (D\to E)\to F.$$ (Where I understand $A\to B\to C$ as $A\to (B\to C)$, in case that is relevant.) There might be information ...
1answer
56 views

### Natural numbers as types.

My question could be simple but I haven't found an answer for it: could we define a type theory where the types are the natural numbers themselves (not the set of the natural numbers)? Thanks.
1answer
166 views

### How to understand inductive definitions of recursive data types?

The problem was encountered when learning Computability Notes by Roberto Zunino (link), page 9 and 11. It seems as if it is a well-known issue and I don't need to specify the "canonical" meaning of ...
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 21, "mathjax_display_tex": 1, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9054675102233887, "perplexity_flag": "middle"}