---

Step * 1 of Lemma ps-sigma-elim-equality-rule2


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. T : {X.Σ A B ⊢ _}
6. t1 : {X.A.B ⊢ _:(T)SigmaUnElim}
7. t2 : {X.Σ A B ⊢ _:T}
8. t1 = (t2)SigmaUnElim ∈ {X.A.B ⊢ _:(T)SigmaUnElim}
⊢ (t1)SigmaElim = t2 ∈ {X.Σ A B ⊢ _:T}
BY
{ ApFunToHypEquands `Z' ⌜(Z)SigmaElim⌝ ⌜{X.Σ A B ⊢ _:T}⌝ (-1)⋅ }

1
.....fun wf..... 
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. T : {X.Σ A B ⊢ _}
6. t1 : {X.A.B ⊢ _:(T)SigmaUnElim}
7. t2 : {X.Σ A B ⊢ _:T}
8. t1 = (t2)SigmaUnElim ∈ {X.A.B ⊢ _:(T)SigmaUnElim}
9. Z : {X.A.B ⊢ _:(T)SigmaUnElim}
⊢ (Z)SigmaElim = (Z)SigmaElim ∈ {X.Σ A B ⊢ _:T}

2
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. T : {X.Σ A B ⊢ _}
6. t1 : {X.A.B ⊢ _:(T)SigmaUnElim}
7. t2 : {X.Σ A B ⊢ _:T}
8. t1 = (t2)SigmaUnElim ∈ {X.A.B ⊢ _:(T)SigmaUnElim}
9. (t1)SigmaElim = ((t2)SigmaUnElim)SigmaElim ∈ {X.Σ A B ⊢ _:T}
⊢ (t1)SigmaElim = t2 ∈ {X.Σ A B ⊢ _:T}

---

Latex:

---

Latex:

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.  t1  :  \{X.A.B  \mvdash{}  \_:(T)SigmaUnElim\}
7.  t2  :  \{X.\mSigma{}  A  B  \mvdash{}  \_:T\}
8.  t1  =  (t2)SigmaUnElim
\mvdash{}  (t1)SigmaElim  =  t2


By

---

Latex:
ApFunToHypEquands  `Z'  \mkleeneopen{}(Z)SigmaElim\mkleeneclose{}  \mkleeneopen{}\{X.\mSigma{}  A  B  \mvdash{}  \_:T\}\mkleeneclose{}  (-1)\mcdot{}

---

Home Index