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
39 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
16 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
48 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
21 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
96 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
45 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
46 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
32 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
46 views

Where to study type theory? [on hold]

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
73 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
26 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
70 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
56 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
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 ...
1
vote
2answers
35 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
0answers
122 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
93 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
127 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
65 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
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
92 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
50 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
56 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
101 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
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
54 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
63 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
300 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
31 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
69 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 ...
11
votes
2answers
520 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 ...
5
votes
0answers
61 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} = ...
6
votes
1answer
125 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
78 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 ...
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 ...
3
votes
2answers
66 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 ...
10
votes
2answers
368 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 ...
2
votes
1answer
71 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
125 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 ...
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 ...
1
vote
1answer
53 views

What is the 'type' of a natural transformation

Let $C,D$ be categories with objects $O_C,O_D$ and morphisms $M_C:O_C\times O_C\to Type_0$, $M_D:O_D\times O_D\to Type_0$. Let $F,G:C\to D$ be functors. A natural transformation $\eta$ associates to ...
1
vote
0answers
25 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 $$ ...
0
votes
1answer
35 views

Type theoretic existential introduction and proof with subtypes

I'm working through a book[1], on type theory and categorial grammar (for linguistic applications). Sadly, I ran into problems pretty early on. I'd be very grateful if someone could Explain the ...
3
votes
0answers
71 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
0answers
42 views

When is the higher-order theory of a model categorical?

I'm interested in (classical) type theories $L$ with the following property. For $M$ any model of $L$ (in Set), let $T(M)$ be the type theory of $M$, i.e., the strongest extension of $L$ satisfied by ...
3
votes
2answers
132 views

Types versus kinds and sorts

In the context of logic, especially Higher‑Order‑Logic and Calculus‑of‑Construction, what is a kind and how does it relates to and differs from a type? My raw guess if that a kind is the higher level ...
2
votes
0answers
124 views

Continuations vs. Yoneda

There is this observation (worldpress blog) that the continuation monad (Wikipedia) stems from the Yoneda embedding. For fixed data types $R$, the monad maps data types $T$ to types $(T\to R)\to R$. ...
0
votes
0answers
31 views

Proper terminology for a pair of magmas

Given two magmas, call them $f$ and $g$ over the same set $a$, what do I call a tuple $h$ of them? With extra properties we call them such names as fields and rings. I am just looking for the generic ...
8
votes
1answer
143 views

How to prove that these are the only type inhabitants?

Consider a type $$\mathsf{Boolean} = \forall \alpha.\ \alpha \to \alpha \to \alpha$$ with its two inhabitants \begin{align} \mathrm{tt} &= \lambda x.\ \lambda y.\ x \\ \mathrm{ff} &= \lambda ...