Communities

Writing
Writing
Codidact Meta
Codidact Meta
The Great Outdoors
The Great Outdoors
Photography & Video
Photography & Video
Scientific Speculation
Scientific Speculation
Cooking
Cooking
Electrical Engineering
Electrical Engineering
Judaism
Judaism
Languages & Linguistics
Languages & Linguistics
Software Development
Software Development
Mathematics
Mathematics
Christianity
Christianity
Code Golf
Code Golf
Music
Music
Physics
Physics
Linux Systems
Linux Systems
Power Users
Power Users
Tabletop RPGs
Tabletop RPGs
Community Proposals
Community Proposals
tag:snake search within a tag
answers:0 unanswered questions
user:xxxx search by author id
score:0.5 posts with 0.5+ score
"snake oil" exact phrase
votes:4 posts with 4+ votes
created:<1w created < 1 week ago
post_type:xxxx type of post
Search help
Notifications
Mark all as read See all your notifications »
Users Search
Help Dashboard Sign In Sign Up
Q&A Meta
Q&A
Posts Tags Edits
Ask Question

Post History

60%
+1 −0
Q&A Defining the two universes from Calculus of Constructions in LF

0 answers  ·  posted 1y ago by user205‭  ·  edited 1y ago by user205‭

Question type-theory logic
#4: Post edited by user avatar user205‭ · 2023-03-30T22:08:56Z (over 1 year ago)
  • Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes are from [here][1].
  • >LF is a simple type system with terms of the following forms:
  • >$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$
  • >where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.
  • (Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)
  • It has [these judgements][2] and [these][3] and [these][4] inference rules.
  • > In the logical framework, there is a special kind $\textbf{Type}$, each of whose objects $A$ generates a kind $El(A)$. When specifying a type theory in LF, $\textbf{Type}$ corresponds to the conceptual universe of types of the type theory to be specified, and for any type $A$, i.e., any object of kind $\textbf{Type}$, kind $El(A)$ corresponds to the collection of objects of type $A$.
  • I was wondering how we could specify something like the Calculus of Constructions (or something close to it) in this LF? At the very least we should have two "things", $\ast$ and $\square$, such that $\ast: \square$. Sometimes $\ast$ is referred to as the type of all types (which I interpret as a universe of level zero), and $\square$ as the type of all kinds (which I interpret as a universe of level one). [This note][5] talks about defining universes in LF. To match its notation, let $U_0 = \ast, U_1 = \square$. Then, as suggested on page 3, we need to introduce constants
  • $$U_0 : \textbf{Type}, \
  • T_0: (U_0)\textbf{Type}, \ u_0: U_1, \ U_1:\textbf{Type}, T_1: (U_1)\textbf{Type}, $$ and assert the computation rule $T_1(u_0)=U_0 : \textbf{Type}$
  • Is this how it's done? But I never used $El(A)$ here, is it not needed for universe specification? I mean, $El$ corresponds to $T_0$, as noted in [this answer](https://math.codidact.com/posts/287995/288005#answer-288005), but if we can just introduce a constant named $T_0$ (and $T_1$), do we not need $El$ at all? In fact, it seems $T_0$ not used at all (unlike $T_1$ which is used in the assertion $T_1(u_0)=U_0 : \textbf{Type}$). But then I don't understand the purpose of adding $El(A)$ in the list of admissible terms of LF...
  • Further, [this answer](https://math.codidact.com/posts/287995/288005#answer-288005) also says that $U_0$ corresponds to $\textbf{Type}$, does this mean that we should have $U_0=\textbf{Type}$ instead of $U_0=\ast$? (Maybe this is not a good question, but I just want to show which aspects made me confused.)
  • Lastly, this may be a topic for a separate question (feel free to ignore it in this question, I can ask about that separately), but there are 2 or 4 variations for most inference rules in CoC. Here's a [picture][6] from the book "Type theory and formal proof"; each of $s_1, s_2, $ and $s$ can be either $\ast$ or $\square$. How do inference rules in LF account for all these variations (assuming that we know how to introduce pi and lambdas - this is done [here][7])? After introducing the constants for pi and lambda, and declaring appropriate computation rules, I thought only one set of inference rules will follow from LF's inference rulles.
  • [1]: https://global.oup.com/academic/product/computation-and-reasoning-9780198538356?cc=us&lang=en&
  • [2]: https://i.stack.imgur.com/N7tOU.png
  • [3]: https://i.stack.imgur.com/CpaoL.png
  • [4]: https://i.stack.imgur.com/NHhx0.png
  • [5]: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf
  • [6]: https://i.stack.imgur.com/IQHlJ.png
  • [7]: https://i.stack.imgur.com/q2VZx.png
  • Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes are from [here][1].
  • >LF is a simple type system with terms of the following forms:
  • >$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$
  • >where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.
  • (Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)
  • It has [these judgements][2] and [these][3] and [these][4] inference rules.
  • > In the logical framework, there is a special kind $\textbf{Type}$, each of whose objects $A$ generates a kind $El(A)$. When specifying a type theory in LF, $\textbf{Type}$ corresponds to the conceptual universe of types of the type theory to be specified, and for any type $A$, i.e., any object of kind $\textbf{Type}$, kind $El(A)$ corresponds to the collection of objects of type $A$.
  • I was wondering how we could specify something like the Calculus of Constructions (or something close to it) in this LF? At the very least we should have two "things", $\ast$ and $\square$, such that $\ast: \square$. Sometimes $\ast$ is referred to as the type of all types (which I interpret as a universe of level zero), and $\square$ as the type of all kinds (which I interpret as a universe of level one). [This note][5] talks about defining universes in LF. To match its notation, let $U_0 = \ast, U_1 = \square$. Then, as suggested on page 3, we need to introduce constants
  • $$U_0 : \textbf{Type}, \
  • T_0: (U_0)\textbf{Type}, \ u_0: U_1, \ U_1:\textbf{Type}, T_1: (U_1)\textbf{Type}, $$ and assert the computation rule $T_1(u_0)=U_0 : \textbf{Type}$
  • Is this how it's done? But I never used $El(A)$ here, is it not needed for universe specification? I mean, $El$ corresponds to $T_0$, as noted in [this answer](https://math.codidact.com/posts/287995/288005#answer-288005), but if we can just introduce a constant named $T_0$ (and $T_1$), do we not need $El$ at all? In fact, it seems $T_0$ not used at all (unlike $T_1$ which is used in the assertion $T_1(u_0)=U_0 : \textbf{Type}$). But then I don't understand the purpose of adding $El(A)$ in the list of admissible terms of LF...
  • Further, [this answer](https://math.codidact.com/posts/287995/288005#answer-288005) also says that $U_0$ corresponds to $\textbf{Type}$, does this mean that we should have $U_0=\textbf{Type}$ instead of $U_0=\ast$? (Maybe this is not a good question, but I just want to show which aspects made me confused.)
  • Lastly, this may be a topic for a separate question (feel free to ignore it in this question, I can ask about that separately), but there are 2 or 4 variations for most inference rules in CoC. Here's a [picture][6] from the book "Type theory and formal proof"; each of $s_1, s_2, $ and $s$ can be either $\ast$ or $\square$. How do inference rules in LF account for all these variations (assuming that we know how to introduce pi and lambdas - this is done [here][7])? After introducing the constants for pi and lambda, and declaring appropriate computation rules, I thought only one set of inference rules will follow from LF's inference rulles (and that one set will correspond to $s_1=s_2=\ast$ as far as I understand).
  • [1]: https://global.oup.com/academic/product/computation-and-reasoning-9780198538356?cc=us&lang=en&
  • [2]: https://i.stack.imgur.com/N7tOU.png
  • [3]: https://i.stack.imgur.com/CpaoL.png
  • [4]: https://i.stack.imgur.com/NHhx0.png
  • [5]: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf
  • [6]: https://i.stack.imgur.com/IQHlJ.png
  • [7]: https://i.stack.imgur.com/q2VZx.png
#3: Post edited by user avatar user205‭ · 2023-03-30T22:06:30Z (over 1 year ago)
  • Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes are from [here][1].
  • >LF is a simple type system with terms of the following forms:
  • >$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$
  • >where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.
  • (Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)
  • It has [these judgements][2] and [these][3] and [these][4] inference rules.
  • > In the logical framework, there is a special kind $\textbf{Type}$, each of whose objects $A$ generates a kind $El(A)$. When specifying a type theory in LF, $\textbf{Type}$ corresponds to the conceptual universe of types of the type theory to be specified, and for any type $A$, i.e., any object of kind $\textbf{Type}$, kind $El(A)$ corresponds to the collection of objects of type $A$.
  • I was wondering how we could specify something like the Calculus of Constructions (or something close to it) in this LF? At the very least we should have two "things", $\ast$ and $\square$, such that $\ast: \square$. Sometimes $\ast$ is referred to as the type of all types (which I interpret as a universe of level zero), and $\square$ as the type of all kinds (which I interpret as a universe of level one). [This note][5] talks about defining universes in LF. To match its notation, let $U_0 = \ast, U_1 = \square$. Then, as suggested on page 3, we need to introduce constants
  • $$U_0 : \textbf{Type}, \
  • T_0: (U_0)\textbf{Type}, \ u_0: U_1, \ U_1:\textbf{Type}, T_1: (U_1)\textbf{Type}, $$ and assert the computation rule $T_1(u_0)=U_0 : \textbf{Type}$
  • Is this how it's done? But I never used $El(A)$ here, is it not needed for universe specification? I mean, $El$ corresponds to $T_0$, as noted in [this answer](https://math.codidact.com/posts/287995/288005#answer-288005), but if we can just introduce a constant named $T_0$ (and $T_1$), do we not need $El$ at all? But then I don't understand the purpose of adding $El(A)$ in the list of admissible terms of LF...
  • Also, is $T_0$ not used at all?
  • Further, [this answer](https://math.codidact.com/posts/287995/288005#answer-288005) also says that $U_0$ corresponds to $\textbf{Type}$, does this mean that we should have $U_0=\textbf{Type}$ instead of $U_0=\ast$? (Maybe this is not a good question, but I just want to show which aspects made me confused.)
  • Lastly, this may be a topic for a separate question (feel free to ignore it in this question, I can ask about that separately), but there are 2 or 4 variations for most inference rules in CoC. Here's a [picture][6] from the book "Type theory and formal proof"; each of $s_1, s_2, $ and $s$ can be either $\ast$ or $\square$. How do inference rules in LF account for all these variations (assuming that we know how to introduce pi and lambdas - this is done [here][7])? After introducing the constants for pi and lambda, and declaring appropriate computation rules, I thought only one set of inference rules will follow from LF's inference rulles.
  • [1]: https://global.oup.com/academic/product/computation-and-reasoning-9780198538356?cc=us&lang=en&
  • [2]: https://i.stack.imgur.com/N7tOU.png
  • [3]: https://i.stack.imgur.com/CpaoL.png
  • [4]: https://i.stack.imgur.com/NHhx0.png
  • [5]: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf
  • [6]: https://i.stack.imgur.com/IQHlJ.png
  • [7]: https://i.stack.imgur.com/q2VZx.png
  • Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes are from [here][1].
  • >LF is a simple type system with terms of the following forms:
  • >$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$
  • >where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.
  • (Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)
  • It has [these judgements][2] and [these][3] and [these][4] inference rules.
  • > In the logical framework, there is a special kind $\textbf{Type}$, each of whose objects $A$ generates a kind $El(A)$. When specifying a type theory in LF, $\textbf{Type}$ corresponds to the conceptual universe of types of the type theory to be specified, and for any type $A$, i.e., any object of kind $\textbf{Type}$, kind $El(A)$ corresponds to the collection of objects of type $A$.
  • I was wondering how we could specify something like the Calculus of Constructions (or something close to it) in this LF? At the very least we should have two "things", $\ast$ and $\square$, such that $\ast: \square$. Sometimes $\ast$ is referred to as the type of all types (which I interpret as a universe of level zero), and $\square$ as the type of all kinds (which I interpret as a universe of level one). [This note][5] talks about defining universes in LF. To match its notation, let $U_0 = \ast, U_1 = \square$. Then, as suggested on page 3, we need to introduce constants
  • $$U_0 : \textbf{Type}, \
  • T_0: (U_0)\textbf{Type}, \ u_0: U_1, \ U_1:\textbf{Type}, T_1: (U_1)\textbf{Type}, $$ and assert the computation rule $T_1(u_0)=U_0 : \textbf{Type}$
  • Is this how it's done? But I never used $El(A)$ here, is it not needed for universe specification? I mean, $El$ corresponds to $T_0$, as noted in [this answer](https://math.codidact.com/posts/287995/288005#answer-288005), but if we can just introduce a constant named $T_0$ (and $T_1$), do we not need $El$ at all? In fact, it seems $T_0$ not used at all (unlike $T_1$ which is used in the assertion $T_1(u_0)=U_0 : \textbf{Type}$). But then I don't understand the purpose of adding $El(A)$ in the list of admissible terms of LF...
  • Further, [this answer](https://math.codidact.com/posts/287995/288005#answer-288005) also says that $U_0$ corresponds to $\textbf{Type}$, does this mean that we should have $U_0=\textbf{Type}$ instead of $U_0=\ast$? (Maybe this is not a good question, but I just want to show which aspects made me confused.)
  • Lastly, this may be a topic for a separate question (feel free to ignore it in this question, I can ask about that separately), but there are 2 or 4 variations for most inference rules in CoC. Here's a [picture][6] from the book "Type theory and formal proof"; each of $s_1, s_2, $ and $s$ can be either $\ast$ or $\square$. How do inference rules in LF account for all these variations (assuming that we know how to introduce pi and lambdas - this is done [here][7])? After introducing the constants for pi and lambda, and declaring appropriate computation rules, I thought only one set of inference rules will follow from LF's inference rulles.
  • [1]: https://global.oup.com/academic/product/computation-and-reasoning-9780198538356?cc=us&lang=en&
  • [2]: https://i.stack.imgur.com/N7tOU.png
  • [3]: https://i.stack.imgur.com/CpaoL.png
  • [4]: https://i.stack.imgur.com/NHhx0.png
  • [5]: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf
  • [6]: https://i.stack.imgur.com/IQHlJ.png
  • [7]: https://i.stack.imgur.com/q2VZx.png
#2: Post edited by user avatar user205‭ · 2023-03-30T21:52:44Z (over 1 year ago)
  • Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes are from [here][1].
  • >LF is a simple type system with terms of the following forms:
  • >$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$
  • >where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.
  • (Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)
  • It has [these judgements][2] and [these][3] and [these][4] inference rules.
  • > In the logical framework, there is a special kind $\textbf{Type}$, each of whose objects $A$ generates a kind $El(A)$. When specifying a type theory in LF, $\textbf{Type}$ corresponds to the conceptual universe of types of the type theory to be specified, and for any type $A$, i.e., any object of kind $\textbf{Type}$, kind $El(A)$ corresponds to the collection of objects of type $A$.
  • I was wondering how we could specify something like the Calculus of Constructions (or something close to it) in this LF? At the very least we should have two "things", $\ast$ and $\square$, such that $\ast: \square$. Sometimes $\ast$ is referred to as the type of all types (which I interpret as a universe of level zero), and $\square$ as the type of all kinds (which I interpret as a universe of level one). [This note][5] talks about defining universes in LF. To match its notation, let $U_0 = \ast, U_1 = \square$. Then, as suggested on page 3, we need to introduce constants
  • $$U_0 : \textbf{Type}, \
  • T_0: (U_0)\textbf{Type}, \ u_0: U_1, \ U_1:\textbf{Type}, T_1: (U_1)\textbf{Type}, $$ and assert the computation rule $T_1(u_0)=U_0 : \textbf{Type}$
  • Is this how it's done? But I never used $El(A)$ here, is it not needed for universe specification? I mean, $El$ corresponds to $T_0$, as noted in [this answer](https://math.codidact.com/posts/287995/288005#answer-288005), but if we can just introduce a constant named $T_0$ (and $T_1$), do we not need $El$ at all? But then I don't understand the purpose of adding $El(A)$ in the list of admissible terms of LF...
  • Also, is $T_0$ not used at all?
  • Lastly, this may be a topic for a separate question (feel free to ignore it in this question, I can ask about that separately), but there are 2 or 4 variations for most inference rules in CoC. Here's a [picture][6] from the book "Type theory and formal proof"; each of $s_1, s_2, $ and $s$ can be either $\ast$ or $\square$. How do inference rules in LF account for all these variations (assuming that we know how to introduce pi and lambdas - this is done [here][7])? After introducing the constants for pi and lambda, and declaring appropriate computation rules, I thought only one set of inference rules will follow from LF's inference rulles.
  • [1]: https://global.oup.com/academic/product/computation-and-reasoning-9780198538356?cc=us&lang=en&
  • [2]: https://i.stack.imgur.com/N7tOU.png
  • [3]: https://i.stack.imgur.com/CpaoL.png
  • [4]: https://i.stack.imgur.com/NHhx0.png
  • [5]: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf
  • [6]: https://i.stack.imgur.com/IQHlJ.png
  • [7]: https://i.stack.imgur.com/q2VZx.png
  • Consider LF, the logical framework used to define UTT (unified theory of dependent types). The next two quotes are from [here][1].
  • >LF is a simple type system with terms of the following forms:
  • >$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$
  • >where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively.
  • (Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)
  • It has [these judgements][2] and [these][3] and [these][4] inference rules.
  • > In the logical framework, there is a special kind $\textbf{Type}$, each of whose objects $A$ generates a kind $El(A)$. When specifying a type theory in LF, $\textbf{Type}$ corresponds to the conceptual universe of types of the type theory to be specified, and for any type $A$, i.e., any object of kind $\textbf{Type}$, kind $El(A)$ corresponds to the collection of objects of type $A$.
  • I was wondering how we could specify something like the Calculus of Constructions (or something close to it) in this LF? At the very least we should have two "things", $\ast$ and $\square$, such that $\ast: \square$. Sometimes $\ast$ is referred to as the type of all types (which I interpret as a universe of level zero), and $\square$ as the type of all kinds (which I interpret as a universe of level one). [This note][5] talks about defining universes in LF. To match its notation, let $U_0 = \ast, U_1 = \square$. Then, as suggested on page 3, we need to introduce constants
  • $$U_0 : \textbf{Type}, \
  • T_0: (U_0)\textbf{Type}, \ u_0: U_1, \ U_1:\textbf{Type}, T_1: (U_1)\textbf{Type}, $$ and assert the computation rule $T_1(u_0)=U_0 : \textbf{Type}$
  • Is this how it's done? But I never used $El(A)$ here, is it not needed for universe specification? I mean, $El$ corresponds to $T_0$, as noted in [this answer](https://math.codidact.com/posts/287995/288005#answer-288005), but if we can just introduce a constant named $T_0$ (and $T_1$), do we not need $El$ at all? But then I don't understand the purpose of adding $El(A)$ in the list of admissible terms of LF...
  • Also, is $T_0$ not used at all?
  • Further, [this answer](https://math.codidact.com/posts/287995/288005#answer-288005) also says that $U_0$ corresponds to $\textbf{Type}$, does this mean that we should have $U_0=\textbf{Type}$ instead of $U_0=\ast$? (Maybe this is not a good question, but I just want to show which aspects made me confused.)
  • Lastly, this may be a topic for a separate question (feel free to ignore it in this question, I can ask about that separately), but there are 2 or 4 variations for most inference rules in CoC. Here's a [picture][6] from the book "Type theory and formal proof"; each of $s_1, s_2, $ and $s$ can be either $\ast$ or $\square$. How do inference rules in LF account for all these variations (assuming that we know how to introduce pi and lambdas - this is done [here][7])? After introducing the constants for pi and lambda, and declaring appropriate computation rules, I thought only one set of inference rules will follow from LF's inference rulles.
  • [1]: https://global.oup.com/academic/product/computation-and-reasoning-9780198538356?cc=us&lang=en&
  • [2]: https://i.stack.imgur.com/N7tOU.png
  • [3]: https://i.stack.imgur.com/CpaoL.png
  • [4]: https://i.stack.imgur.com/NHhx0.png
  • [5]: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf
  • [6]: https://i.stack.imgur.com/IQHlJ.png
  • [7]: https://i.stack.imgur.com/q2VZx.png
#1: Initial revision by user avatar user205‭ · 2023-03-30T21:46:23Z (over 1 year ago) 
Defining the two universes from Calculus of Constructions in LF
Consider LF, the logical framework used to define UTT  (unified theory of dependent types). The next two quotes are from [here][1].

>LF is a simple type system with terms of the following forms: 
>$$\textbf {Type}, El(A), (x:K)K', [x:K]k', f(k),$$
>where the free occurences of variable $x$ in $K'$ and $k'$ are bound by the binding operators $(x:K)$ and $[x:K]$, respectively. 

(Note:$[x:K]b$ means $\lambda x:K. b$ and $(x:K)K'$ means $\Pi x:K.K'$.)

It has [these judgements][2] and [these][3] and [these][4] inference rules.

> In the logical framework, there is a special kind $\textbf{Type}$, each of whose objects $A$ generates a kind $El(A)$. When specifying a type theory in LF, $\textbf{Type}$ corresponds to the conceptual universe of types of the type theory to be specified, and for any type $A$, i.e., any object of kind $\textbf{Type}$, kind $El(A)$ corresponds to the collection of objects of type $A$.

I was wondering how we could specify something like the Calculus of Constructions (or something close to it) in this LF? At the very least we should have two "things", $\ast$ and $\square$, such that $\ast: \square$. Sometimes $\ast$ is referred to as the type of all types (which I interpret as a universe of level zero), and $\square$ as the type of all kinds (which I interpret as a universe of level one).  [This note][5] talks about defining universes in LF. To match its notation, let $U_0 = \ast, U_1 = \square$. Then, as suggested on page 3, we need to introduce constants



$$U_0 : \textbf{Type}, \ 
T_0: (U_0)\textbf{Type}, \ u_0: U_1, \ U_1:\textbf{Type}, T_1: (U_1)\textbf{Type}, $$ and assert the computation rule $T_1(u_0)=U_0 : \textbf{Type}$



Is this how it's done? But I never used $El(A)$ here, is it not needed for universe specification? I mean, $El$ corresponds to $T_0$, as noted in [this answer](https://math.codidact.com/posts/287995/288005#answer-288005), but if we can just introduce a constant named $T_0$ (and $T_1$), do we not need $El$ at all? But then I don't understand the purpose of adding $El(A)$ in the list of admissible terms of LF...

Also, is $T_0$ not used at all?

Lastly, this may be a topic for a separate question (feel free to ignore it in this question, I can ask about that separately), but there are 2 or 4 variations for most inference rules in CoC. Here's a [picture][6] from the book "Type theory and formal proof"; each of $s_1, s_2, $ and $s$ can be either $\ast$ or $\square$. How do inference rules in LF account for all these variations (assuming that we know how to introduce pi and lambdas - this is done [here][7])? After introducing the constants for pi and lambda, and declaring appropriate computation rules, I thought only one set of inference rules will follow from LF's inference rulles. 


  [1]: https://global.oup.com/academic/product/computation-and-reasoning-9780198538356?cc=us&lang=en&
  [2]: https://i.stack.imgur.com/N7tOU.png
  [3]: https://i.stack.imgur.com/CpaoL.png
  [4]: https://i.stack.imgur.com/NHhx0.png
  [5]: https://www.cs.rhul.ac.uk/home/zhaohui/universes.pdf
  [6]: https://i.stack.imgur.com/IQHlJ.png
  [7]: https://i.stack.imgur.com/q2VZx.png
type-theory logic