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

2
votes
2answers
958 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 ...
16
votes
3answers
696 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 ...
9
votes
1answer
304 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 ...
3
votes
2answers
130 views

Is there a (foundational) type theory with the features I'm looking for?

I like to distinguish between sets and subsets. We imagine that sets are floating free in the universe, and that the elements of a set are constructed according to some kind of recursive rules. Like ...
6
votes
3answers
267 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 ...
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 ...
3
votes
0answers
67 views

What is the desirable function identification when setting up arrows in the category of types?

My question is which functions can not be allowed in a statically typed programming language, so that the "canonical" category is less coarse than what you get if you define it's arrows to be ...
2
votes
2answers
123 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 ...
0
votes
1answer
225 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 ...