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

3
votes
1answer
76 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 ...
2
votes
0answers
18 views

Disequality in Type Theory [duplicate]

Is it possible to prove $0 \neq 1$ in (non-univalent) Martin-Löf type theory, where $0$ and $1$ are natural numbers (defined using the usual inductive type $0 : \mathbb{N}$, $S : \mathbb{N} \to ...
13
votes
1answer
352 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. ...
6
votes
1answer
41 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 ...
1
vote
1answer
36 views

Why does the dependent product type need “forall”?

I feel stupid asking this question because it is so fundamental to logic and math. However, in my starting to learn proof theory and now type theory, I have not seen an explanation on why you need the ...
2
votes
2answers
74 views

How to construct a term of a particular type

I am reading the article "Introduction to Type Theory" by Herman Geuvers, the chapter explaining the Fitch style of natural inference. I stuck at the exercise 1.3 (first two are simple): ...
2
votes
0answers
29 views

Proof by reflection and Homotopy Type Theory

I have been looking into various proof assistants, and came across the method of proof by reflection in Coq, which (from what I understand) allows one to verify a program provides the correct "answer" ...
4
votes
0answers
38 views

Where to study type theory?

I want to learn more about (homotopy) type theory, constructive mathematics and univalent foundations. To my knowledge, there are only few faculties with large type theory groups. In Europe, most of ...
2
votes
2answers
66 views

Logic vs. type system

What's the difference between logic (in a narrow sense, i.e. a logical system such as ZOL, FOL, etc.) and type system? I will sketch my understanding of this -- please correct if I err. Under ...
11
votes
2answers
515 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 ...
2
votes
1answer
23 views

Introductory Type Theory Questions

My textbook(Pierce's Types and Programming Languages defines $\mathbb{B}$(untyped) our language as consisting of the terms $True$, $False$, and $if\ t_{1}\ then\ t_{2}\ else\ t_{3}$ and the ...
1
vote
1answer
68 views

Mistake in http://plato.stanford.edu/entries/type-theory/#2

There seems to be mistake in http://plato.stanford.edu/entries/type-theory/#2: First-order logic considers only types of the form $i,…,i → i$ (type of function symbols), and $i,…,i → o$ ...
3
votes
2answers
266 views

Has a Dependent Type always a Type?

I am experimenting with dependent types. Lets assume the following short notation: ...
4
votes
1answer
52 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 ...
1
vote
2answers
32 views

Self-application in Church's untyped lambda calculus

In "Proposition as Types" by Philip Wadler mentions the weaknesses of untyped lambda calculus and "Russell's logic" concerning self-application. Whereas self-application in Russell’s logic leads ...
3
votes
2answers
76 views

Are untyped and simply typed lambda calculus mutually exclusive?

In "Proposition as Types" by Philip Wadler we can read that: The two applications of lambda calculus, to represent computation and to represent logic, are in a sense mutually exclusive. If ...
3
votes
0answers
115 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 ...
10
votes
2answers
333 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 ...
0
votes
1answer
79 views

Define inl : $σ → σ ∨ τ$

I'm a bit stuck in Geuvers' "Introduction to Type Theory" (http://www.cs.ru.nl/~herman/onderwijs/provingwithCA/paper-lncs.pdf), p. 39: Exercise 13. Prove the derivability of some of the other logical ...
4
votes
2answers
113 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 ...
2
votes
1answer
95 views

Do I really need lambda abstraction for type theory?

So I think I somewhat understand the type theory of the various lambda calculi in the lambda cube, from the simply typed lambda calculus to the calculus of constructions, but looking at it I'm ...
6
votes
0answers
49 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 ...
6
votes
3answers
238 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 ...
5
votes
2answers
262 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 ...
3
votes
1answer
59 views

Does type-theory have a concept of “relation”?

Set theory cares about sets and relations. And then functions are relations betweens sets of inputs and outputs. Type theory, on the other hand, seems to say that there are no formal ideas of ...
2
votes
1answer
66 views

Basic concerns about dependent function types

I am working my way through the introductory material of Homotopy Type Theory and by the end of section $1.5$ it is clear that I did not have the earlier material down as clearly as I had thought. I ...
1
vote
0answers
24 views

Proving the Identity Type Has a Term

I am trying to get used to type theory. I have a two things to ask. Let $1$ be the unit type with unique term $\star : 1$. As an exercise I was trying to prove that $$ ...
1
vote
1answer
55 views

Problems with validity in type theory

I'm twisting my brains over some simple formulas in intensional type theory. First: If $\exists x \Box (x=^{\vee}j)$, s.t. $x$ is of type $<e>$ and refers to an entity $e$ and $j$ is of ...
2
votes
1answer
51 views

Two questions about the empty type

I have two questions regarding the empty type, $0$, in Martin-Löf type theory: I was reading that, in intuitionistic logic, one has $\neg\neg\neg P\rightarrow \neg P$. This amounts to finding a ...
6
votes
1answer
124 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 ...
2
votes
1answer
59 views

What's the need for a pair type $A \times B$ in Homotopy Type Theory?

I'm reading the Homotopy Type Theory book and I got confused about the following issue. The book defines a primitive $\Pi$-type as the generalization of the function type. The $\Pi$-type can be ...
1
vote
0answers
28 views

What is the origin of the use of $\Pi$ and $\Sigma$ for dependent function and dependent product types in type theory? [duplicate]

In the type theory I have read (e.g. homotopy type theory) I have seen the following notion used for dependent function types: $$\prod_{x : A} B(x)$$ and the following for dependent product types: ...
4
votes
1answer
91 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
1answer
52 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 ...
3
votes
3answers
74 views

What is a conventional name for a set of values having no properties except that values are distinct?

I know essentially nothing about math but I'm interested in very low-level concepts. I'm thinking of something like a finite or infinite set (although I'm not married to consider sets per se, maybe ...
5
votes
2answers
50 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
0answers
61 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 ...
7
votes
3answers
281 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 ...
2
votes
0answers
30 views

What strongly normalizing lambda calculi exist that can be integrated with/as logic?

If I'm trying to implement a logical system for deduction based on propositional reasoning, I can start with predicates and quantifiers and functions to obtain first order logic. I can further extend ...
5
votes
1answer
68 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
60 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} = ...
2
votes
1answer
76 views

On the definition of a Type

I am working through Spivak's text on category theory and he gives the definition of a type as :"A type is an abstract concept, a distinction the author has made". This seems very informal and after ...
51
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
2answers
64 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 ...
1
vote
1answer
104 views

Find subgraphs in a directed graph which are isolated by edge properties

Please excuse my small knowledge of graph theory vocabulary. I can only describe the problem with common english words. Maybe someone can point me into the right direction and/or terms to look up. ...
2
votes
1answer
70 views

Why are Truth, Conjunction, and Implication called “Negative” fragments of IPL (intuitionisti logic Proposition Logic)?

Someone answered that negative means we are ""Using"" them . But the point is for all of these there is an Introduction rule too. So why call them negative? I don't know whether it's computer ...
2
votes
1answer
124 views

Being contractible in homotopy theory vs. homotopy type theory

I'm trying to clarify the notion of being contractible in homotopy theory vs. homotopy type theory. Is the following right? "In homotopy theory the real interval $[0,1]$, considered as a subset ...
0
votes
1answer
34 views

Reexpressing the higher inductive-inductive surreals with only two mutual subdefinitions

In $\S 11.6$ of the HoTT book, the authors describe Conway's surreal numbers in terms of a higher inductive-inductive definition with three mutual subdefinitions. However, it seems to me that only ...
12
votes
1answer
429 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 ...
1
vote
1answer
51 views

Proof that the empty type exists

Is there a proof that the empty type exists? If there is, it's not in my textbook and I haven't been able to find one online. I feel like if it's impossible to prove the existence of the empty type, ...