---

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


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)SigmaUnElim}
8. t1 = t2 ∈ {X.A.B ⊢ _:(T)SigmaUnElim}
9. (t1)SigmaElim = (t2)SigmaElim ∈ {X.Σ A B ⊢ _:T}
⊢ (t1)SigmaElim = (t2)SigmaElim ∈ {X.Σ A B ⊢ _:T}
BY
{ Auto }

---

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


By

---

Latex:
Auto

---

Home Index