The tag has no wiki summary.

learn more… | top users | synonyms

9
votes
2answers
470 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 ...
11
votes
1answer
317 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. ...
1
vote
0answers
19 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: ...
3
votes
1answer
74 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 ...
3
votes
1answer
36 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 ...
0
votes
0answers
48 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 ...
2
votes
3answers
69 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 ...
3
votes
2answers
38 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 ...
4
votes
0answers
49 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
262 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
58 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 ...
5
votes
0answers
57 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} = ...
4
votes
1answer
103 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
71 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 ...
48
votes
8answers
8k 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 ...
9
votes
2answers
252 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
2answers
55 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 ...
-1
votes
1answer
49 views

problems with validity in type theory

I'm twisting my brains over some simple formulas in intensional type theory. If $\exists x \Box (x=^{\vee}j)$, s.t. $x$ is of type $<e>$ and refers to an entity $e$ and $j$ is of type ...
1
vote
1answer
84 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. ...
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 ...
1
vote
1answer
96 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 ...
0
votes
1answer
33 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 ...
12
votes
1answer
351 views

Type theory as foundations

Does anyone know any good references that describe type theoretical foundations of mathematics? I've read some books e.g. Winskel's The Formal Semantics of Programming Languages and Pierce's Types and ...
1
vote
1answer
43 views

Two questions about the empty type

I have a couple of questions regarding the empty type, $0$, in Martin-Lof type theory. I was reading that, in intuitionistic logic, one has $\neg\neg\neg P\rightarrow \neg P$. This amounts to ...
1
vote
1answer
49 views

Proof that the empty type exists

Is there a proof that the empty type exists? If there is, it's not in my textbook and I haven't been able to find one online. I feel like if it's impossible to prove the existence of the empty type, ...
1
vote
1answer
52 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 ...
0
votes
0answers
21 views

Proving the Identity Type Has a Term

I am trying to get used to type theory. I have a couple of 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
33 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
65 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 ...
1
vote
0answers
40 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
125 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
92 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 ...
3
votes
1answer
90 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 ...
8
votes
4answers
292 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
7
votes
1answer
139 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 ...
2
votes
2answers
119 views

Variables in Types in type theory

I'm slowly grasping this, though the different formulations of type theory make it difficult. In http://imps.mcmaster.ca/doc/seven-virtues.pdf types can only be formed from *, i, and a->b when a and ...
2
votes
1answer
79 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 ...
5
votes
1answer
212 views

Foundational theories, their uses, interactions and comparisons?

Until now, I heard that there are some theories for building mathematical objects (or at least it is what it seems to my poor knowledge). Some of these are: Set theory; Logic; Category theory; Type ...
5
votes
3answers
108 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 ...
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 ...
3
votes
2answers
125 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 ...
0
votes
0answers
35 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 ...
3
votes
1answer
45 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 ...
7
votes
1answer
306 views

Axiom of Choice - Type Theory (Proof)

Background In Intuitionistic Type Theory (p. 27-28), Martin Löf provides a proof of the axiom of choice that is constructively valid. This version is considerably weaker than the ordinary set theory ...
2
votes
1answer
85 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 ...
1
vote
1answer
79 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 ...
2
votes
2answers
848 views

Constructing dependent product (right adjoint to pullback) in a locally cartesian closed category

I've been trying to find a proof that the pullback functors in a locally cartesian closed category have right adjoints (used to model the notion of indexed product inside a category (rather than ...
4
votes
0answers
110 views

W-types and inverse image functor

All sheaf topoi have W-types and in fact there's an explicit construction given by Benno van den Berg & Ieke Moerdijk, but the construction is quite involved. I would like to know whether the ...