---

Step * 1 1 3 of Lemma gen_hyp_tp

.....assertion..... 
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
5. A ∈ Type
6. e ∈ A
⊢ ∀x:A. (e = x ∈ A ∈ Type)
BY
{ (\p.At (get_term_arg `UA` p) (D 0) p) }

1
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
5. A ∈ Type
6. e ∈ A
7. x : A
⊢ e = x ∈ A ∈ Type

2
.....wf..... 
1. A : Type
2. e : A
3. H : A ⟶ 𝕌{j}
4. z : H e
5. A ∈ Type
6. e ∈ A
⊢ istype(A)

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  e  :  A
3.  H  :  A  {}\mrightarrow{}  \mBbbU{}\{j\}
4.  z  :  H  e
5.  A  \mmember{}  Type
6.  e  \mmember{}  A
\mvdash{}  \mforall{}x:A.  (e  =  x  \mmember{}  Type)


By

---

Latex:
(\mbackslash{}p.At  (get\_term\_arg  `UA`  p)  (D  0)  p)

---

Home Index