4
votes
2answers
236 views

Is there a name for relations with this property, and the category of them?

The following math.stackexchange question asked whether there is a name for a certain sort of relation. I have become interested in the question, and no one suggested a name there, so I am asking ...
13
votes
2answers
573 views

$\infty$-categorical interpretation of type theory

One can read at several places that Martin-löf type theory should be the internal language of a locally Cartesian closed infinity category, and that the univalence axiom should distinguished infinity ...
5
votes
1answer
220 views

$\Pi$, $\Sigma$, and identity types without $\eta$ in comprehension categories

In comprehension categories, dependent sums are defined as a choice of left adjoints for all reindexing functors along display maps, satisfying a Beck-Chevalley condition. Dependent products are ...
1
vote
0answers
69 views

Natural relations between substitutions

Consider two contexts $\Gamma,\Delta$ (from some background type theory), and substitutions $s_1,s_2:\Gamma\rightarrow \Delta$. In the case of $1$-element contexts, we get that a substitution is ...
9
votes
2answers
562 views

Category of Judgements?

I have been able to find a lot of information on the category of contexts -- for example, the page on syntactic categories at the nLab is a good starting point. However, when I try to find similar ...
6
votes
2answers
272 views

Why no morphisms from the contradictory proposition to the inconsistent context?

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 question applies to ...
7
votes
2answers
257 views

Categorical semantics of W-types

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 there a similar ...
4
votes
1answer
301 views

What are categorical models of W-types in intensional type theory?

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 intensional case.
12
votes
3answers
2k views

What is the theory of polynomials?

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 universal algebra ...
15
votes
2answers
871 views

Surreal Numbers as Inductive Type?

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 of a universal ...
5
votes
3answers
555 views

What do I call type theory without Curry-Howard?

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 type theories as a ...
3
votes
0answers
193 views

An elegant formulation for typed sets

Fix a poset $T$, which we'll think of as a set of "types," interpreting $a \leq b$ as "$a$ is more general than $b$." Construct a category of TSet as follows. Objects: Pairs ($X$, $\tau : X ...
6
votes
4answers
658 views

What is the intuitive meaning of star and box in a pure type system?

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 meanings of $\star$ and ...
6
votes
2answers
626 views

Recursively dependent types?

Is there such a thing as "recursively dependent types"? Specifically, I would like a dependent type theory containing a type $A(x)$ which depends on a variable $x: A(z)$, where $z$ is a particular ...