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

1
vote
1answer
47 views

How am I to interpret induction/recursion in type theory?

This may have been asked before, but I haven't been able to find it if so. The induction and recursion principles for various types in (for me, at least, homotopy) type theory allow one to define a ...
2
votes
2answers
61 views

How are image and pre-image different from range and domain respectively?

How are image and pre-image different from range and domain respectively, in Layman's terms (as simple as possible)? Are they basically just keywords that often indicate more nuanced subsets of the ...
16
votes
2answers
436 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. ...
2
votes
1answer
38 views

Constructing natural numbers as lists of units (possible infinite objects)

I'm puzzled by this question, which is more about relation between two type theoretic approaches. Nevertheless, It can be shortened to the question : When it is correct (if ever) to construct ...
65
votes
8answers
13k 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 ...
0
votes
2answers
42 views

Group theory vs Type theory

I have to state that I am not very proficient in either one or the other, but at first glance they both seem to tackle similar concepts. Wikipedia's definition of type theory: In mathematics, ...
1
vote
0answers
43 views

Resources for learning functional programming/Haskell for the mathematically inclined.

I am a math student wanting to learn some functional programming with Haskell. From what I understand, many type theory concepts are analogous, even equivalent, to category theory concepts (e.g. ...
2
votes
1answer
90 views

Can type theory be viewed as an alternative to model theory?

While type theory certainly has traditionally been used for different purposes than model theory, as noted in this Philosophy SE post, I wonder to what extent type theory could model model theory ...
0
votes
2answers
48 views

Categorical interpretation of equality type

Consider the Martin Lof type theory. It's know that: product type correspond to product of two obects; unit type correspond to terminal object; and so on. The equality type corresponds to some ...
0
votes
1answer
49 views

Is this a valid representation of real numbers?

I am trying to find the simplest representation of real numbers on the lambda calculus. I've thought about this one, and wonder if this is valid. First, we define a real number in the range ...
4
votes
3answers
161 views

What exactly are the numbers we use everyday?

Pi can be defined as diameter / circunference of a circle. But what is a circle? You can't tell a computer: "build a circle and divide its diameter by its ...
2
votes
5answers
434 views

Type Theory for Beginners

One of the first things one learns at university are some foundations of mathematics. This covers topics such as sets, functions between sets, relations, logic & proof, ... I learned this stuff ...
1
vote
1answer
47 views

Intuitionistic logic unit type as truth

I am trying to learn constructive logic. Why can true be represent as a unit type while false is represented as the void type?
3
votes
1answer
133 views

How are halting oracles related to set theory?

By the Curry Howard isomorphism, constructive type theory and computation are intimately related to mathematical logic and proofs. Moreover, type theory gives us a nice framework for describing ...
0
votes
1answer
73 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 ...
1
vote
2answers
71 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
46 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
143 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
50 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 ...
3
votes
2answers
107 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 : ...
3
votes
1answer
169 views

Give an example of a program in Simply Typed Lambda that produces Bottom.

I'm not sure how bottom applies to simply typed lambda calculus. not A is a common abbreviation for A -> ⊥ But I see no way to construct a function of that signature within the theory. Edit: A more ...
4
votes
1answer
69 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. ...
2
votes
1answer
59 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 ...
2
votes
0answers
20 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 ...
1
vote
1answer
36 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
72 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 ...
-1
votes
1answer
123 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
56 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
60 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
79 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 ...
5
votes
3answers
73 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 ...
3
votes
0answers
45 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
53 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 ...
1
vote
0answers
60 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 : ...
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 ...
6
votes
0answers
84 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
31 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 ...
12
votes
2answers
370 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 ...
12
votes
2answers
654 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 ...
3
votes
1answer
139 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
33 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 ...
6
votes
1answer
67 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
84 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
80 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): ...
3
votes
0answers
59 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" ...