---

Step * of Lemma ps-sigma-elim-unelim

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].
  (SigmaUnElim o SigmaElim = 1(X.Σ A B) ∈ psc_map{[i | j]:l}(C; X.Σ A B; X.Σ A B))
BY
{ (Auto THEN BLemma `pscm-equal` THEN Auto THEN RepeatFor 2 ((FunExt THENA Auto))) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. I : cat-ob(C)
6. x : X.Σ A B(I)
⊢ (SigmaUnElim o SigmaElim I x) = (1(X.Σ A B) I x) ∈ X.Σ A B(I)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  BLemma  `pscm-equal`  THEN  Auto  THEN  RepeatFor  2  ((FunExt  THENA  Auto)))

---

Home Index