The tag has no wiki summary.

learn more… | top users | synonyms

7
votes
0answers
174 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 ...
0
votes
1answer
57 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
66 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
458 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
90 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 ...
3
votes
0answers
37 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 ...
8
votes
1answer
234 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
0answers
33 views

What if typing judgements were propositions?

Suppose we created a modified type theory in which typing judgments like $x : X$ are not judgments at all; rather, they're propositions. Would this be a bad idea? If so, why? A good answer should ...
2
votes
1answer
55 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
32 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
20 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 ...
0
votes
0answers
33 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 ...
1
vote
0answers
20 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
65 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
2answers
43 views

Construction Types or Type Constructions?

In any (simple) type theory there are base types (i.e. the type of individuals and the type of propositions) and type builders (i.e. $\rightarrow$, which takes two types $t,t'$ and yields the type of ...
0
votes
0answers
14 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 ...
1
vote
1answer
34 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 ...
9
votes
0answers
146 views

Reference on standard types

This question is about what I presume is a basic construction in type theory. The finite types are defined as follows: 0 is a finite type; if $\sigma, \tau$ are finite types, then so is ...
2
votes
2answers
76 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 ...
6
votes
1answer
387 views

Relationship between propositional logic, first-order logic, second-order logic higher-order logic, and type theory

I understand there is propositional logic, first-order logic, second-order logic higher-order logic, and type theory, where the latter logics are extensions of the former logics. Can someone explain ...
1
vote
0answers
31 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, ...
4
votes
3answers
81 views

What's a good resource to learn about the simply typed lambda calculus?

I've read An Introduction to Functional Programming Through Lambda Calculus by Greg Michaelson, and found it to be a very good resource to learn about the untyped lambda calculus. However, I want to ...
3
votes
1answer
160 views

Logic within Type theory. Is there a rough academic consensus on how this should be done?

I guess because of it's presence in several blogs on math and even physics, I've recently started to learn some type theory, often from people who know about it and from books which use it. I want to ...
5
votes
3answers
178 views

Introductory books as preparation to read Voevodsky homotopy-theory (HoTT) book

I would like to read Voevodsky HoTT book. However, I lack a lot of the basics. I would need a few introductory books first that cover topics like groupoids, fibrations, W -types, Homotopy theory. ...
2
votes
1answer
142 views

How to represent Smullyan's “Mockingbird” puzzles in (Homotopy) Type Theory?

(If you're unfamiliar with the puzzles from To Mock a Mockingbird, three pages tell you everything you should need.) Is it possible to solve the riddles in To Mock a Mockingbird in a "propositions as ...
3
votes
2answers
155 views

How to understand the definition of sets in homotopy type theory and the role of univalence?

Bear with me, I'm a physicist. In homotopy type theory, as I understand it, a type $X$ is a set if all the morphisms over its terms $x:X$ are identies. When I say "morphisms", then I view the term as ...
2
votes
0answers
44 views

Set Theory - Well Order (Lexiographical combination)

Question: Prove constructively that if $(A_{1},\prec_{1})$ and $(A_{2},\prec_{2})$ are two well-ordered sets then their lexicographical combination $(A_{1} \times A_{2},<_{1,2})$ is also well ...
4
votes
1answer
81 views

How to describe free magmas in more structuralist terms?

Given a generating set $G$ (assume for simplicitly it consists entirely of urelements), the free magma on $G$ can be described concretely as follows. Its underlying set is the least $U \supseteq G$ ...
1
vote
1answer
37 views

Basic concerns about dependent function types

I am working my way through the introductory material of Homotopy Type Theory and by the end of section $1.5$ it is clear that I did not have the earlier material down as clearly as I had thought. I ...
4
votes
1answer
103 views

How does type theory handle division by zero and such?

Say I have a program that needs to not divide by zero: f(x): if nonzero(x): return sin(x)/x else: return 1 If we divide by zero, we get ...
3
votes
1answer
99 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 ...
14
votes
3answers
552 views

What good is infinity?

I am becoming increasingly convinced that Wildberger's views are, if a little bizarre, at least not hopelessly inconsistent. When I was reading the comments in the video following (MF17), somebody ...
5
votes
0answers
104 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 ...
7
votes
3answers
144 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 ...
2
votes
1answer
82 views

Unprovable Equivalence in Type Theory

Let $\prec$ be a binary relation on a set $A$… A predicate $P(x)$ set $(x:A)$ is said to be progressive with respect to $(A,\prec)$ if \begin{equation} (\forall a:A)\Big((\forall b:A)\big(b \prec a ...
1
vote
2answers
83 views

Explanation of math statement

This symbols are used to describe left recursion : $A\to B\,\alpha\,|\,C$$B\to A\,\beta\,|\,D,$ It is taken from : http://en.wikipedia.org/wiki/Left_recursion How can these symbols be ...
1
vote
1answer
59 views

In type theory, why isn't $x = x' : X$ simply wrong?

If $X$ is a set, then personally, I tend to think of the equality relation on $X$ as a function $X^2 \rightarrow \mathrm{Bool}.$ Following this intuition, think that if $x$ and $y$ are variables of ...
4
votes
0answers
143 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 ...
4
votes
1answer
96 views

Curry-Howard Correspondence (Proof Theory)

As you all know, the Curry-Howard correspondance provides a link between type theory and predicate logic. Concepts featured in the former, such as $\Pi$-type and $\Sigma$-type can, by the ...
2
votes
1answer
84 views

Struggling with classes

I am still struggling with the concept of classes in ZF set theory. From Jech, Set Theory, p.5: That means: For every formula $\varphi(x)$ there is a class (which is definable). There are ...
11
votes
3answers
352 views

Why is it worth spending time on type theory?

Looking around there are three candidates for "foundations of mathematics": set theory category theory type theory There is a seminal paper relating these three topics: From Sets to Types to ...
3
votes
3answers
184 views

Book on lambda calculus logic and type theory

Can someone recommend me a book for self study which will cover topics of logic, lambda calculus and type theory. I know about "Computability and Logic" written by Bolos but it describe recursive ...
1
vote
1answer
57 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): ...
6
votes
1answer
170 views

Confusion about Homotopy Type Theory terminology

I've picked up the Homotopy Type Theory book for leisure. I'm comfortable with strongly typed languages and familiar with dependently typed languages and I enjoy topology, so I thought that the HoTT ...
4
votes
2answers
123 views

Is higher order type theory the same as higher order logic?

The internal language of a topos is higher order intuitionistic type theory (or logic). Here the higher order simply refers to allowing function types. In mathematical logic we have higher-order ...
5
votes
1answer
156 views

Difference between a type and a set

I've been trying to understand this distinction for a while, buts its still not making sense to me. Originally, I thought the distinction between type and set was as follows. The relationship ...
0
votes
1answer
67 views

What can be proven within Simply Typed lambda calculus?

I was reading http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus and I'm having a hard time thinking of anything remotely interesting that can be proven within Simply Typed lambda calculus. Am ...
1
vote
1answer
50 views

Left Inclusion is Not Equal to Right Inclusion

I am reading through a type theory book and gave myself the following problem: Let $A$ be a type. Then we have the coproduct type $A+A$. I want to show that left inclusion $l(a)$ is not equal to ...
1
vote
2answers
97 views

What does $x : X$ mean?

I've tried to learn type theory a few times, but the notation $x : X$ always trips me up. Does it mean: $x$ represents a fixed but arbitrary inhabitant of the type $X$? The variable $x$ is just ...
5
votes
2answers
87 views

Is there a theory of extensible definitions?

We can define $+$ as a function $\mathbb{N}^2 \rightarrow \mathbb{N}$, and then prove: Theorem 1. The range of $+$ is $\mathbb{N}$. If we later wish to extend $+$ to a function $\mathbb{Z}^2 ...