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 tags:...

learn more… | top users | synonyms

2
votes
0answers
28 views

Are the 1 dimensional loop spaces in homotopy type theory commutative?

Theorem 2.1.6 of the Homotopy Type Theory book proves that $\Omega^{2}A$ is always commutative, using a similar argument to the one used for loop spaces in algebraic topology. Isn't it also the case (...
5
votes
1answer
83 views

Categorical semantics explained – what is an interpretation?

I’ve been really having a hard time trying to understand categorical semantics. In fact, I am confused to the point I am afraid I don't know how to ask this question! I’ve been reading textbooks like ...
5
votes
2answers
83 views

Formal systems in which $\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$ is true, but the contrapositive is disallowed.

Question. Are there any formal systems out there for which $$\forall x \in \mathbb{R}(x \neq 0 \rightarrow x^{-1} \neq 0)$$ is true, but the contrapositive $$\forall x \in \mathbb{R}(x^{-1} =...
-1
votes
0answers
110 views

Implicit arguments in informal math, how to explain?

Let we have three categories $Z$, $C$, and $D$. And let $Z$ have partially ordered Hom-sets each Hom-set having a least element. Let also every object of $D$ be an ordered set and has least element. I ...
0
votes
0answers
26 views

Is an assumption of P[x/x] equivelant to P?

I'm doing problem 4.13 from https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf (p95) where the objective is to prove $\neg (\exists x : X).P \Leftrightarrow (\forall x : X).\neg P$. Is https://...
3
votes
1answer
91 views

Formalizing splitting into cases

Let $x$ denote a fixed but arbitrary real, and suppose we're trying to solve an equation like $$(x^2-1)^2 = 1.$$ The 'high school' approach is to just shuffle the functions on one side onto the other ...
15
votes
2answers
452 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. ...
0
votes
0answers
24 views

reflexive-transitive closure of --->, how to understand that?

given term t and t', decide whether t --->* t' -/->, where --->* is the reflexive-transitive closure of --->. Above two lines are from a paper about programming language meta-theory. I did not ...
1
vote
1answer
39 views

What does $0^-$ mean in set or type theory?

In "A Unification Algorithm for COQ Featuring Universe Polymorphism and Overloading", Ziliani and Sozeau say: Terms include variables $x \in \mathcal{V}$, constants $c \in > \mathcal{C}$, ...
7
votes
1answer
90 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 ...
0
votes
1answer
55 views

Is the Identity Type an Identity Function?

Definition 1. Given a set $S$, the identity function on $S$ is the function $id_S:S \to S$ that maps any element $x \in S$ to itself. Proposition. Given a type $S$, the identity type for $S$ is the ...
2
votes
0answers
75 views

What is the relationship between Realizability and the Curry-Howard isomorphism?

I have recently been studying the Curry-Howard isomorphism/correspondence. My sources have primarly been Sørensen [1] and Girard [2]. Realizability is introduced here in the form of Kleene's ...
3
votes
0answers
27 views

What to call a term-in-context whose context contains exactly the variables occurring in the term?

In type theory, a term-in-context $\Gamma \vdash t : \tau $ is only well-formed when $\Gamma$ contains all the variables occurring in $t:\tau$. Is there a name for when it contains exactly the ...
1
vote
1answer
54 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
72 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 ...
2
votes
1answer
39 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 ...
68
votes
8answers
14k 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
64 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
51 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
61 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
54 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
167 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
515 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
52 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
135 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
78 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
75 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
49 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
147 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
53 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
113 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
170 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
61 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 propositions-as-...
2
votes
0answers
26 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
126 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
26 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
59 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
65 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
92 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
2answers
78 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
47 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 ...
1
vote
0answers
59 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
62 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
61 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 ...