---

Step * of Lemma pscm-presheaf-sigma

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 o p;q) ∈ {Delta ⊢ _})
BY
{ (Auto THEN BLemma `presheaf-type-equal` THEN Try (Complete (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)
⊢ (Σ A B)s
= Σ (A)s (B)(s o p;q)
∈ (A:I:cat-ob(C) ⟶ Delta(I) ⟶ Type × (I:cat-ob(C)
                                       ⟶ J:cat-ob(C)
                                       ⟶ f:(cat-arrow(C) J I)
                                       ⟶ a:Delta(I)
                                       ⟶ (A I a)
                                       ⟶ (A J f(a))))

---

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  o  p;q))


By

---

Latex:
(Auto  THEN  BLemma  `presheaf-type-equal`  THEN  Try  (Complete  (Auto)))

---

Home Index