---

Step * of Lemma pscm-presheaf-sigma-typed

No Annotations
∀C:SmallCategory. ∀X,Delta:ps_context{j:l}(C). ∀A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀s:psc_map{j:l}(C; Delta; X).
  ((Σ A B)s = Σ (A)s (B)(s)dep ∈ {Delta ⊢ _})
BY
{ (Intros THEN (Assert (B)(s)dep ∈ Delta.(A)s ⊢  BY Auto)) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. A : {X ⊢ _}
5. B : {X.A ⊢ _}
6. s : psc_map{j:l}(C; Delta; X)
7. (B)(s)dep ∈ Delta.(A)s ⊢ 
⊢ (Σ A B)s = Σ (A)s (B)(s)dep ∈ {Delta ⊢ _}

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}X,Delta:ps\_context\{j:l\}(C).  \mforall{}A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.
\mforall{}s:psc\_map\{j:l\}(C;  Delta;  X).
    ((\mSigma{}  A  B)s  =  \mSigma{}  (A)s  (B)(s)dep)


By

---

Latex:
(Intros  THEN  (Assert  (B)(s)dep  \mmember{}  Delta.(A)s  \mvdash{}    BY  Auto))

---

Home Index