---

Step * of Lemma presheaf-app-id-fun

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A:{X ⊢ _}]. ∀[u:{X ⊢ _:A}].  (app(presheaf-id-fun(X); u) = u ∈ {X ⊢ _:A})
BY
{ (Auto
   THEN Unfold `presheaf-id-fun` 0
   THEN Unfold `presheaf-lam` 0
   THEN (InstLemma `presheaf-beta` [⌜C⌝;⌜X⌝;⌜A⌝;⌜(A)p⌝;⌜q⌝;⌜u⌝]⋅ THENA Auto)) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. u : {X ⊢ _:A}
5. app((λq); u) = (q)[u] ∈ {X ⊢ _:((A)p)[u]}
⊢ app((λq); u) = u ∈ {X ⊢ _:A}

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `presheaf-id-fun`  0
  THEN  Unfold  `presheaf-lam`  0
  THEN  (InstLemma  `presheaf-beta`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index