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

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. ...
4
votes
1answer
128 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
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 ...
11
votes
0answers
189 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 ...
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 ...
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 ...
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} = ...
4
votes
0answers
77 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 ...
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 ...
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 ...
3
votes
0answers
89 views

Are large cardinals bi-interperable with type theory?

"Sets in Types, Types in Sets" establishes that the calculus of constructions is bi-interpretable with ZFC + infinitely many inaccessibles. Are there any more results like this higher up the large ...
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 ...
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 ...
2
votes
0answers
43 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
0answers
61 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 ...
2
votes
0answers
77 views

What are the main differences between set theory versus pure type systems?

According to wikipedia, a pure type system: ...is a form of typed lambda calculus that allows an arbitrary number of sorts and dependencies between any of these... Pure type systems may ...
2
votes
0answers
85 views

Introductory text about different stratification methods in higher-order logic and set theory

Could someone recommend me a good overview text about stratification of predicates, comprehension axioms, and other methods of avoiding the paradoxes in untyped or only loosely/relatively typed ...
1
vote
0answers
23 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 $$ ...
1
vote
0answers
100 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$. ...
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 ...
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
0answers
49 views

Enumeration of symbols in grammatical expressions or vertices in tree graphs

I have expressions (type of a function) like e.g. $$f:(A\to B)\to C \to (D\to E)\to F.$$ (Where I understand $A\to B\to C$ as $A\to (B\to C)$, in case that is relevant.) There might be information ...
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 ...
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 ...