---

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


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{[i | j]:l}(C; X.Σ A B; X.Σ A B)
6. T : {X.Σ A B ⊢ _}
7. (T)SigmaUnElim o SigmaElim = (T)1(X.Σ A B) ∈ {X.Σ A B ⊢ _}
⊢ ((T)SigmaUnElim)SigmaElim = T ∈ {X.Σ A B ⊢ _}
BY
{ (NthHypEqGen (-1) THEN EqCDA THEN Auto) }

---

Latex:

---

Latex:

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)SigmaUnElim  o  SigmaElim  =  (T)1(X.\mSigma{}  A  B)
\mvdash{}  ((T)SigmaUnElim)SigmaElim  =  T


By

---

Latex:
(NthHypEqGen  (-1)  THEN  EqCDA  THEN  Auto)

---

Home Index