---

Step * of Lemma presheaf-sigma-p-p

No Annotations
∀C:SmallCategory. ∀X:ps_context{j:l}(C). ∀T,A:{X ⊢ _}. ∀B:{X.A ⊢ _}. ∀E:{X.T ⊢ _}.
  (((Σ A B)p)p = Σ ((A)p)p (B)(p o p o p;q) ∈ {X.T.E ⊢ _})
BY
{ (Auto
   THEN (InstLemma `pscm-presheaf-sigma` [⌜parm{i}⌝;⌜parm{i|j}⌝;⌜C⌝;⌜X⌝;⌜X.T.E⌝;⌜A⌝;⌜B⌝;⌜p o p⌝]⋅ THENA Auto)
   THEN NthHypSq (-1)
   THEN PscmUnfolding
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}X:ps\_context\{j:l\}(C).  \mforall{}T,A:\{X  \mvdash{}  \_\}.  \mforall{}B:\{X.A  \mvdash{}  \_\}.  \mforall{}E:\{X.T  \mvdash{}  \_\}.
    (((\mSigma{}  A  B)p)p  =  \mSigma{}  ((A)p)p  (B)(p  o  p  o  p;q))


By

---

Latex:
(Auto
  THEN  (InstLemma  `pscm-presheaf-sigma`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}X.T.E\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}p  o  p\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  NthHypSq  (-1)
  THEN  PscmUnfolding
  THEN  Auto)

---

Home Index