---

Step * of Lemma presheaf-term-equal2

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[u,z:{X ⊢ _:A}].
  u = z ∈ {X ⊢ _:A} supposing ∀I:cat-ob(C). ∀a:X(I).  ((u I a) = (z I a) ∈ A(a))
BY
{ (Auto THEN EqTypeCD THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[u,z:\{X  \mvdash{}  \_:A\}].
    u  =  z  supposing  \mforall{}I:cat-ob(C).  \mforall{}a:X(I).    ((u  I  a)  =  (z  I  a))


By

---

Latex:
(Auto  THEN  EqTypeCD  THEN  Auto)

---

Home Index