---

Step * of Lemma presheaf-sigma-intro

No Annotations
∀C:SmallCategory. ∀G:ps_context{j:l}(C). ∀A:{G ⊢ _}. ∀B:{G.A ⊢ _}.  ((∃a:{G ⊢ _:A}. {G ⊢ _:(B)[a]}) ⇒ {G ⊢ _:Σ A B})
BY
{ (Intros THEN ExRepD THEN RenameVar  `b' (-1) THEN UseWitness ⌜presheaf-pair(a;b)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}C:SmallCategory.  \mforall{}G:ps\_context\{j:l\}(C).  \mforall{}A:\{G  \mvdash{}  \_\}.  \mforall{}B:\{G.A  \mvdash{}  \_\}.
    ((\mexists{}a:\{G  \mvdash{}  \_:A\}.  \{G  \mvdash{}  \_:(B)[a]\})  {}\mRightarrow{}  \{G  \mvdash{}  \_:\mSigma{}  A  B\})


By

---

Latex:
(Intros  THEN  ExRepD  THEN  RenameVar    `b'  (-1)  THEN  UseWitness  \mkleeneopen{}presheaf-pair(a;b)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index