---

Step * 1 of Lemma ps-sigma-elim-rule

.....subterm..... T:t
3:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. T : {X.Σ A B ⊢ _}
6. t : {X.A.B ⊢ _:(T)SigmaUnElim}
7. (t)SigmaElim ∈ {X.Σ A B ⊢ _:((T)SigmaUnElim)SigmaElim}
⊢ ((T)SigmaUnElim)SigmaElim = T ∈ presheaf-type{[j | i]:l}(C; X.Σ A B)
BY
{ (RWO "pscm-ap-comp-type<" 0 THENA Auto) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. T : {X.Σ A B ⊢ _}
6. t : {X.A.B ⊢ _:(T)SigmaUnElim}
7. (t)SigmaElim ∈ {X.Σ A B ⊢ _:((T)SigmaUnElim)SigmaElim}
⊢ (T)SigmaUnElim o SigmaElim = T ∈ presheaf-type{[j | i]:l}(C; X.Σ A B)

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  T  :  \{X.\mSigma{}  A  B  \mvdash{}  \_\}
6.  t  :  \{X.A.B  \mvdash{}  \_:(T)SigmaUnElim\}
7.  (t)SigmaElim  \mmember{}  \{X.\mSigma{}  A  B  \mvdash{}  \_:((T)SigmaUnElim)SigmaElim\}
\mvdash{}  ((T)SigmaUnElim)SigmaElim  =  T


By

---

Latex:
(RWO  "pscm-ap-comp-type<"  0  THENA  Auto)

---

Home Index