---

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

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[T:{X.Σ A B ⊢ _}].
  (((T)SigmaUnElim)SigmaElim = T ∈ {X.Σ A B ⊢ _})
BY
{ (InstLemma `ps-sigma-elim-unelim` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (ApFunToHypEquands `Z' ⌜(T)Z⌝ ⌜{X.Σ A B ⊢ _}⌝ (-2)⋅ THENA Auto)) }

1
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 ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[B:\{X.A  \mvdash{}  \_\}].  \mforall{}[T:\{X.\mSigma{}  A  B  \mvdash{}  \_\}].
    (((T)SigmaUnElim)SigmaElim  =  T)


By

---

Latex:
(InstLemma  `ps-sigma-elim-unelim`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}(T)Z\mkleeneclose{}  \mkleeneopen{}\{X.\mSigma{}  A  B  \mvdash{}  \_\}\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto))

---

Home Index