Consider Higher order predicate logic over dependent type theory (DPL) as defined in Chapter 11 of B. Jacobs's book "Categorical Logic and Type Theory" (though I think this questio …

Jacob's book titled "Categorical Logic and Type Theory" gives a nice description of Π and Σ types as adjunctions to substitution functors induced by display maps. Is ther …

Prompted by James Propp's recent question about surreal numbers, I was wondering whether anyone had investigated the idea of describing surreal numbers (as ordered class) in terms …

(I'm not sure if I should post this here rather than at Theoretical Computer Science, I've found a lot of type theory related questions on MathOverflow) I'm working in Martin-Löf …

I'm familiar with container functors and older work by Dybjer on categorical models for W-types in the extensional theory, but I was looking for some similar semantics in the inten …

We all know what polynomials are, along with their elementary properties and many effective algorithms for different representations of polynomials. The question here is more of a …

Less tongue in cheek, is it known what the relative consistency is for theorems proved with an automatic theorem prover? Of course this depends somewhat on what assumptions one mak …

In trying to understand homotopy type theory, I stumbled upon the following silly question, which is likely to be trivial for the experts. Let $B=\sqcup_{n\in\Bbb N} BS_n$, which …

The systems of the λ-cube have the axiom $\star:\square$. I've listed a few meanings that the Curry-Howard isomorphism gives to $t : T$ below. What are the intuitive meani …

Define the axiom constants $p_{A,B}^{((A\rightarrow B)\rightarrow A)\rightarrow A}$ as realizers of the Peirce formula, and $f_A^{\bot\rightarrow A}$ as realizers of the Ex Falso Q …

Mathematically, I know what a semigroup is: It is a set S along with an associative binary operation $* : S \times S \rightarrow S$. So far, so good. From a computational perspe …

So I'm not much of a math guy but I've really enjoyed programming in Lisp and have become interested in the ideas of lambda calculus which it is based. I was wondering if anyone h …

I am interested in learning the theory of types, especially in how they can provide a foundation to mathematics different to sets and how they can avoid self-referential paradoxes …

Is there a word I can say which will convey to type theorists that I am not thinking about types as propositions? Background: as a category theorist, I am mostly interested in typ …

Hi all, what are the best strategies to find cutting edge papers and books on a field of mathematics? .. Example: 2-3 years ago I had to analyze a time series. I found a paper …