---

Step * of Lemma presheaf-pi-implies-sigma

No Annotations
∀C:SmallCategory. ∀G:ps_context{j:l}(C). ∀A:{G ⊢ _}. ∀B:{G.A ⊢ _}.  ({G ⊢ _:A} ⇒ {G ⊢ _:ΠA B} ⇒ {G ⊢ _:Σ A B})
BY
{ (Intros
   THEN RenameVar  `a' (-2)
   THEN RenameVar  `b' (-1)
   THEN InstLemma `presheaf-sigma-intro` [⌜C⌝;⌜G⌝;⌜A⌝;⌜B⌝]⋅
   THEN Auto
   THEN D 0 With ⌜a⌝ 
   THEN Auto
   THEN InstLemma `presheaf-app_wf` [⌜C⌝;⌜G⌝;⌜A⌝;⌜B⌝;⌜b⌝;⌜a⌝]⋅
   THEN Auto
   THEN UseWitness ⌜app(b; a)⌝⋅
   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{}  \_\}.
    (\{G  \mvdash{}  \_:A\}  {}\mRightarrow{}  \{G  \mvdash{}  \_:\mPi{}A  B\}  {}\mRightarrow{}  \{G  \mvdash{}  \_:\mSigma{}  A  B\})


By

---

Latex:
(Intros
  THEN  RenameVar    `a'  (-2)
  THEN  RenameVar    `b'  (-1)
  THEN  InstLemma  `presheaf-sigma-intro`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  D  0  With  \mkleeneopen{}a\mkleeneclose{} 
  THEN  Auto
  THEN  InstLemma  `presheaf-app\_wf`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}G\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  UseWitness  \mkleeneopen{}app(b;  a)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index