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
47 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
44 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
21 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
80 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
47 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
38 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
85 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
71 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 ...
4
votes
2answers
43 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
54 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 ...
6
votes
3answers
267 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
29 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
61 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 ...
10
votes
2answers
483 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
58 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} = ...
5
votes
1answer
116 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
73 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
61 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
265 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 ...
2
votes
1answer
68 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
110 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
50 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
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 $$ ...
0
votes
1answer
34 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
67 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
129 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 ...
1
vote
0answers
101 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
140 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 ...
3
votes
1answer
85 views

How do definitions work in Martin-Lof type theory?

The classical viewpoint is that we can found mathematics by specifying a formal system $F$ whose theorems are precisely those of ZFC. However, since $F$ has essentially no support for the concept of a ...
1
vote
1answer
85 views

Typed Category Theory?

This small book (or long paper) describes objects and morphisims in a cateogry as having types. He also talks about pre-categories as categories with typeless objects and morphisims. While I am ...
0
votes
0answers
36 views

Using types instead for basic proofs

Disclaimer: I know close to nothing about formal type theory, but I program intensively so prefer to think in terms of types. In typical math you write $a \in A$ to speak of the nature of your ...
6
votes
3answers
116 views

Types, Sets and Categories

I am learning Category Theory and at first I just pictured a category like a class in object oriented programming: type definition + methods (morphisms). However the author I am reading uses maps ...
3
votes
2answers
130 views

Is there a (foundational) type theory with the features I'm looking for?

I like to distinguish between sets and subsets. We imagine that sets are floating free in the universe, and that the elements of a set are constructed according to some kind of recursive rules. Like ...
4
votes
1answer
46 views

Basic Propositional Logic

I'm working through Thompson's Type Theory and Functional Programming. I've only read the first chapter and want to make sure I'm understanding the material. The first problem asks to prove the ...
3
votes
1answer
86 views

Do we lose everything, if the natural transformations in a monad are exactly inverse?

I'm currently explaining monads $$T:{\bf C}\to{\bf C},\hspace{1cm}\eta:1_{\bf C}\to T,\hspace{1cm}\mu:T\circ T\to T,$$ to my brain and the "only" tricky thing are really the identity relations. I ...
2
votes
1answer
80 views

How to extract the sets “produced” by a axiomatic set theory, into some newly introduced collection?

Say I know well how to reason in a set theory, which for the sake of this question I'll call $\bf{ST}$, say one of those, it can by $\bf ZFC$. It's principally written down via first order logic and ...
4
votes
0answers
81 views

Logic in closed symmetric monoidal categories; reference request.

Suppose we want an algebraic theory $T$ to be interpretable in any closed symmetric monoidal category $\mathbf{C}.$ I am thinking in particular of the case where $\mathbf{C}$ is the category of models ...
1
vote
1answer
89 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. ...
0
votes
1answer
32 views

A class of “internal” endofunctors in cartesian closed categories

I'm interested in a class of endofunctors on cartesian closed categories with a quite natural definition, and am wondering whether/where this class has been studied so far (and how it is called). Fix ...
1
vote
0answers
52 views

Proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in $\lambda\pi $ calculus $\equiv$

What is the right representation of the proof of $(\forall x. \varepsilon(x)) \Rightarrow \bot $ in simple type theory as a term of $\lambda\pi $ calculus $\equiv$? Note on notation: The epsilon ...
2
votes
1answer
97 views

Simple type theory: Proof inexistance of closed term

In simple type theory, how can I prove that there is no closed term of type? $$((P \Rightarrow Q) \Rightarrow Q) \Rightarrow P$$
1
vote
0answers
40 views

Reductions under lambda in dependently typed lambda calculus

I am currently reading a Simon Thompson's Type Theory book. In chapter 5 he introduces a system TT(0,C), which limits a notion of reduction . In this notion of reduction, reductions under lambda are ...
1
vote
1answer
69 views

Is there a notion of property of a mathematical object?

I have an alphabet or set of symbols $\Sigma$ from which I can build sequences of symbols in $\Sigma^+$ (think of sentences of characters). Now I have a function ...
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 ...
4
votes
2answers
240 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
92 views

Is it possible to express sigma-type in Martin-Löf type theory with other constructs

In Martin-Löf type theory we have sigma types (dependent products). Is it possible to express them with other constructs? How expressive is dependently typed lambda calculus without them, i.e. what we ...