---

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

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}]. ∀[T:{X.Σ A B ⊢ _}]. ∀[t:{X.Σ A B ⊢ _:T}].
  (((t)SigmaUnElim)SigmaElim = t ∈ {X.Σ A B ⊢ _:T})
BY
{ (InstLemma `ps-sigma-elim-unelim` []
   THEN RepeatFor 4 (ParallelLast')
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN StrengthenEquation (-3)
   THEN ApFunToHypEquands `Z' ⌜(t)Z⌝ ⌜{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. SigmaUnElim o SigmaElim = 1(X.Σ A B) ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B)
6. T : {X.Σ A B ⊢ _}
7. t : {X.Σ A B ⊢ _:T}
8. SigmaUnElim o SigmaElim
= 1(X.Σ A B)
∈ {z:psc_map{j:l}(C; X.Σ A B; X.Σ A B)| 
   (z = SigmaUnElim o SigmaElim ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))
   ∧ (z = 1(X.Σ A B) ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))} 
9. Z : {z:psc_map{j:l}(C; X.Σ A B; X.Σ A B)| 
        (z = SigmaUnElim o SigmaElim ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))
        ∧ (z = 1(X.Σ A B) ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))} 
⊢ (t)Z = (t)Z ∈ {X.Σ A B ⊢ _:T}

2
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{j:l}(C; X.Σ A B; X.Σ A B)
6. T : {X.Σ A B ⊢ _}
7. t : {X.Σ A B ⊢ _:T}
8. SigmaUnElim o SigmaElim
= 1(X.Σ A B)
∈ {z:psc_map{j:l}(C; X.Σ A B; X.Σ A B)| 
   (z = SigmaUnElim o SigmaElim ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))
   ∧ (z = 1(X.Σ A B) ∈ psc_map{j:l}(C; X.Σ A B; X.Σ A B))} 
9. (t)SigmaUnElim o SigmaElim = (t)1(X.Σ A B) ∈ {X.Σ A B ⊢ _:T}
⊢ ((t)SigmaUnElim)SigmaElim = t ∈ {X.Σ A B ⊢ _:T}

---

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{}  \_\}].
\mforall{}[t:\{X.\mSigma{}  A  B  \mvdash{}  \_:T\}].
    (((t)SigmaUnElim)SigmaElim  =  t)


By

---

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

---

Home Index