Post History
#2: Post edited
by
user205
·
2023-03-27T03:09:40Z (over 1 year ago)
- I'm looking at [this note](https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf) about universes in type theory.
- For Tarski-style universes (page 2), as far as I understand, the "$a$" in $a:U_i$ are formal names of types, whereas the "$T_i(a)$" in $T_i(a) \ type$ are actual types. What I don't understand is the purpose of "$u_i:U_{i+1}$" and "$T_{i+1}(u_i)=U_i$". Is there any intuitive explanation on why we have these two "axioms" (or whatever)?
- Further, it is said in the remark on page 3 that Tarski-style universes can be formulated in LF:
- > $U_i: \textbf{Type}; \ T_i: (U_i)\textbf{Type};\ u_i:U_{i+1};\ T_{i+1}(u_i)=U_i : \textbf{Type}$
But how is this related $El(A)$ from the LF mentioned in [my previous question](https://math.codidact.com/posts/287991)? Is there any relationship between $El(-)$ and $T_j(-)$?
- I'm looking at [this note](https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf) about universes in type theory.
- For Tarski-style universes (page 2), as far as I understand, the "$a$" in $a:U_i$ are formal names of types, whereas the "$T_i(a)$" in $T_i(a) \ type$ are actual types. What I don't understand is the purpose of "$u_i:U_{i+1}$" and "$T_{i+1}(u_i)=U_i$". Is there any intuitive explanation on why we have these two "axioms" (or whatever)?
- Further, it is said in the remark on page 3 that Tarski-style universes can be formulated in LF:
- > $U_i: \textbf{Type}; \ T_i: (U_i)\textbf{Type};\ u_i:U_{i+1};\ T_{i+1}(u_i)=U_i : \textbf{Type}$
- But how is this related to $El(A)$ from the LF mentioned in [my previous question](https://math.codidact.com/posts/287991)? Is there any relationship between $El(-)$ and $T_j(-)$?
#1: Initial revision
by
user205
·
2023-03-27T03:09:09Z (over 1 year ago)
On Tarski-style universes in type theory
I'm looking at [this note](https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf) about universes in type theory.
For Tarski-style universes (page 2), as far as I understand, the "$a$" in $a:U_i$ are formal names of types, whereas the "$T_i(a)$" in $T_i(a) \ type$ are actual types. What I don't understand is the purpose of "$u_i:U_{i+1}$" and "$T_{i+1}(u_i)=U_i$". Is there any intuitive explanation on why we have these two "axioms" (or whatever)?
Further, it is said in the remark on page 3 that Tarski-style universes can be formulated in LF:
> $U_i: \textbf{Type}; \ T_i: (U_i)\textbf{Type};\ u_i:U_{i+1};\ T_{i+1}(u_i)=U_i : \textbf{Type}$
But how is this related $El(A)$ from the LF mentioned in [my previous question](https://math.codidact.com/posts/287991)? Is there any relationship between $El(-)$ and $T_j(-)$?