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

0
votes
1answer
18 views

Distinguishing pure, closed lambda terms

Let $M$ be a full model of the simply typed lambda calculus, over some collection of base types, with the constraint that $|D_\sigma|\geq 2$ for each base type $\sigma$. Let $a$ and $b$ be two closed ...
3
votes
1answer
34 views

How do dependent products in category theory relate to type theory?

I feel like I understand the construction of dependent product types relatively well, it makes sense to me how the introduction and elimination rules work together to create the concept of a function ...
2
votes
2answers
44 views

Type theoretic proof that $\lnot (A \lor B) \Rightarrow \lnot A \land \lnot B$

I'm currently giving the Homotopy Type Theory book a go, and have made it to the section (of Chapter 1) on Propositions as Types. It leaves as an exercise for the reader the proof that $$ ((A + B)\to ...
0
votes
0answers
47 views

Is there a sense in which a formal theory can be more or less “metamathematically aware”?

For example, in classical logic, because of the law of the excluded middle, all propositions must be true or false, so in order to prove that a proposition is actually independent of the theory, we ...
3
votes
2answers
90 views

Definition of “set” in HoTT

In the homotopy type theory book (https://hott.github.io/book/nightly/hott-online-1007-ga1d0d9d.pdf) "set" is defined as follows (see chapter 3): Definition 3.1.1. A type A is a set if for all x, y : ...
4
votes
1answer
63 views

Is the 1-tuple (x) = x?

Based on following sentence In type theory, commonly used in programming languages, a tuple has a product type; this fixes not only the length, but also the underlying types of each component. ...
0
votes
0answers
47 views

Turnstile (\vdash) in adjoint functor and type theory.

Is common symbol $\vdash$ an abuse of notation or there is a deep sacred connection between $$\Gamma \vdash \lambda(a:A).a:\Pi(a:A).A$$ which is preorder and $$G \vdash F \quad \mbox{($F$ is left ...
1
vote
1answer
34 views

How to call a type that can be added / subtracted / divided / multiplied?

Is there something as the quality of something that can be added? Like "addable" or "joinable". For example, numbers can be added, sets can be added, vectors can be added. What is the name of that ...
2
votes
1answer
66 views

Finding a type such that $X + 1 \not\simeq X$ and $X+2\simeq X$

Yesterday, I read the following question : Finding a space such that $X\cong X+2$ and $X\not\cong X+1$, and found the result very astounding. Does it still hold in homotopy type theory? As a type ...
2
votes
0answers
18 views

Consistency of Martin-Löf Type Theory and Categorical Models

Having read the parts of the hott book that introduce intuitionistic type theory (+univalence), I want to continue by studying some meta theory. I'm particularly interested in strategies for proving ...
2
votes
1answer
56 views

Best way to introduce Curry-Howard isomorphism

I want to give a small talk about the Curry-Howard isomorphism to people who are not familiar with intuitionistic logic. Personally, I think about intuitionistic logic just in the ...
-1
votes
1answer
114 views

Axiom of choice in HoTT without sethood requirement

3.8.3 of the HoTT book gives the following as a variant of the axiom of choice: $\Pi$ (X : U) (Y : X $\rightarrow$ U), (isSet X) $\rightarrow$ ($\Pi$ (x : X), isSet (Y x)) $\rightarrow$ ($\Pi$ (x ...
3
votes
0answers
25 views

Extensionality of a hierarchy of functionals over $\mathbb{N}$

Let $H$ be the complete hierarchy of functionals over $\mathbb{N}$. To be precise: let the set $T$ of 'simple types' be the smallest set such that '0' $\in T$ and $(α→β) \in T$ whenever $α, β \in T$. ...
0
votes
1answer
54 views

Does propositional resizing preserve truth of propositions in HoTT?

According to Axiom 3.5.5 of the HoTT book, we have propositional resizing if there is a some f and H such that f : Prop$_u$$_{_i}$ $\rightarrow$ Prop$_u$$_{_{i+1}}$ H : isequiv(f) The idea ...
2
votes
1answer
57 views

Book on Curry-Howard Isomorphisms

I would like to learn about Curry-Howard Isomorphism because I want to know more about connections between computability and logic. I have already read book on first order logic and I know about ...
1
vote
1answer
65 views

Intensional vs. extensional equality (or something like this)

I'm reading this thesis by Michael Warren on Homotopy Type Theory. I'm really a newbie to the field and got puzzled right in the beginning, where the following rule appears: A little bit before he ...
3
votes
0answers
42 views

Contrapositive in Type Theory

We define $\neg P=P\rightarrow 0$ in Martin-Lof type theory. So, we have a function $$ (P\to Q)\to [(Q\to 0)\to (P \to 0)] $$ given by function composition. Am I right that there is not reverse ...
0
votes
0answers
24 views

Syntax in Robert Harper's book

I'm trying to read Practical Foundations For Programming Languages by Robert Harper, especially I'm interested in existential types. So I started with this introduction: In the beginning I was ...
0
votes
0answers
45 views

Category Theory compared with Meta-Grammars (or Hyper-Grammars) in Programming Languages

This may be a simple minded question. First, background: Coming from a linguistic and computer science background, I keep on getting Category Theory shoved, ah, shown to me, when studying both ...
5
votes
3answers
69 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 ...
1
vote
0answers
56 views

Ordinal Numbers within Simple Type Theory

A little preamble: I recently came across the system of higher-order logic known as simple type theory, and I was immediately intrigued by it, as it seemed to be exactly what I was looking for as an ...
1
vote
0answers
60 views

Is this a good way to define “n-paths” in a type?

$\DeclareMathOperator{\succ}{succ}$ Define these two type families by "indexed induction induction." $$\text{_-boundary} : \mathbb{N} \to \mathcal{U} \to \mathcal{U}$$ $$\text{_-path} : \prod_{n : ...
6
votes
0answers
83 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 ...
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 ...
0
votes
0answers
28 views

Structural induction over types that accept functions, in Coq

If you define an inductive type in Coq with a constructor that accepts a function mapping to that type, you get a somewhat odd induction rule. ...
4
votes
1answer
54 views

Why is the rule “If x has type σ in the context, we know that x has type σ” needed?

I am trying to get a deeper understanding of why the rules in logic and type theories exist, and am now looking at the simply typed lambda calculus, the typing rules on Wikipedia. The first one is ...
2
votes
0answers
29 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 ...
3
votes
1answer
126 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 ...
6
votes
1answer
64 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 ...
2
votes
1answer
65 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
0answers
49 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
61 views

Where to study type theory? [closed]

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
91 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 ...
2
votes
1answer
35 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
84 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$ ...
4
votes
1answer
73 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 ...
3
votes
2answers
99 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 ...
1
vote
2answers
67 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 ...
4
votes
0answers
162 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 ...
0
votes
1answer
96 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
165 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 ...
3
votes
1answer
85 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
76 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
31 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
99 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 ...
6
votes
0answers
54 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 ...
4
votes
1answer
81 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 ...
2
votes
1answer
133 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 ...
3
votes
3answers
78 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
64 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 ...