The tag has no wiki summary.

learn more… | top users | synonyms

6
votes
0answers
140 views

What is the most transparent, rigorous definition of the Univalence Axiom?

I've been studying homotopy type theory and trying to grasp the Univalence Axiom. I have yet to find a concise, accessible, rigorous definition of Univalence. I have several excellent survey papers ...
6
votes
0answers
122 views

Preservation of universes in presheaves

In Lifting Grothendieck universes Hofmann and Streicher construct a universe in the category of presheaves over a small category given a Grothendieck universe in $\mathbf{Set}$. Suppose now I have ...
5
votes
0answers
178 views

Feasible Type Theories

I am looking for references about efficient type theories, efficiency in the sense of computational complexity, and type theory in the sense of Martin-Lof's type theories. Has there been any studies ...
3
votes
0answers
81 views

Problem with a proof in Wellfounded trees in categories

I'm reading the paper Wellfounded trees in categories by Moerdijk and Palmgren. I'm having trouble understanding the proof of Theorem 7.2 (page 216), i.e. that in $\mathbf{ML}_{< \omega} ...
3
votes
0answers
94 views

Logical framework for type theories like ML and CIC

I'm looking for a logical framework in which it is possible to easily present both intensional and extensional theories of dependent types with a partially ordered set of universes à la Russell ...
3
votes
0answers
194 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 ...
1
vote
0answers
67 views

Type theory: can multiple elimination rules be defined, in principle?

I'd like to ask a question on type theory: Consider the usual type theoretical definition of the natural numbers. We could give an elimination rule in the form: or in the form: I called the ...
1
vote
0answers
71 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 ...