---

Step * of Lemma pscm-presheaf-id-fun

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[H:ps_context{j:l}(C)]. ∀[s:psc_map{j:l}(C; H; X)].
  ((presheaf-id-fun(X))s = presheaf-id-fun(H) ∈ {H ⊢ _:((A)s ⟶ (A)s)})
BY
{ (Auto
   THEN (InstLemma `pscm-presheaf-lam` [⌜C⌝;⌜X⌝;⌜A⌝;⌜A⌝;⌜q⌝;⌜H⌝;⌜s⌝]⋅ THENA Auto)
   THEN (Subst' (q)s+ ~ q -1 THENA (PscmUnfolding THEN Auto))
   THEN Fold `presheaf-id-fun` (-1)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A:\{X  \mvdash{}  \_\}].  \mforall{}[H:ps\_context\{j:l\}(C)].
\mforall{}[s:psc\_map\{j:l\}(C;  H;  X)].
    ((presheaf-id-fun(X))s  =  presheaf-id-fun(H))


By

---

Latex:
(Auto
  THEN  (InstLemma  `pscm-presheaf-lam`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}H\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  (q)s+  \msim{}  q  -1  THENA  (PscmUnfolding  THEN  Auto))
  THEN  Fold  `presheaf-id-fun`  (-1)
  THEN  Auto)

---

Home Index