---

Step * of Lemma presheaf-sigma_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[B:{X.A ⊢ _}].  (Σ A B ∈ X ⊢ )
BY
{ (Auto THEN Unfold `presheaf-sigma` 0 THEN MemTypeCD THEN Try (MemCD) THEN Reduce 0 THEN Auto) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. I : cat-ob(C)
6. a : X(I)
7. u : u:A(a) × B((a;u))
⊢ <(fst(u) a cat-id(C) I), (snd(u) (a;fst(u)) cat-id(C) I)> = u ∈ (u:A(a) × B((a;u)))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `presheaf-sigma`  0  THEN  MemTypeCD  THEN  Try  (MemCD)  THEN  Reduce  0  THEN  Auto)

---

Home Index