---

Step * 1 of Lemma ps-sigma-unelim-elim-term

.....fun wf..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. SigmaUnElim o SigmaElim = 1(X.Σ A B) ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B)
6. T : {X.Σ A B ⊢ _}
7. t : {X.Σ A B ⊢ _:T}
8. SigmaUnElim o SigmaElim
= 1(X.Σ A B)
∈ {z:psc_map{j:l}(C; X.Σ A B; X.Σ A B)| 
   (z = SigmaUnElim o SigmaElim ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))
   ∧ (z = 1(X.Σ A B) ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))} 
9. Z : {z:psc_map{j:l}(C; X.Σ A B; X.Σ A B)| 
        (z = SigmaUnElim o SigmaElim ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))
        ∧ (z = 1(X.Σ A B) ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))} 
⊢ (t)Z = (t)Z ∈ {X.Σ A B ⊢ _:T}
BY
{ (RepeatFor 2 (D -1) THEN Fold `member` 0 THEN InferEqualTypeUp THEN Auto THEN EqCDA) }

---

Latex:

---

Latex:
.....fun  wf..... 
1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  SigmaUnElim  o  SigmaElim  =  1(X.\mSigma{}  A  B)
6.  T  :  \{X.\mSigma{}  A  B  \mvdash{}  \_\}
7.  t  :  \{X.\mSigma{}  A  B  \mvdash{}  \_:T\}
8.  SigmaUnElim  o  SigmaElim  =  1(X.\mSigma{}  A  B)
9.  Z  :  \{z:psc\_map\{j:l\}(C;  X.\mSigma{}  A  B;  X.\mSigma{}  A  B)|  (z  =  SigmaUnElim  o  SigmaElim)  \mwedge{}  (z  =  1(X.\mSigma{}  A  B))\} 
\mvdash{}  (t)Z  =  (t)Z


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  Fold  `member`  0  THEN  InferEqualTypeUp  THEN  Auto  THEN  EqCDA)

---

Home Index