---

Step * of Lemma presheaf-fun-comp_wf

No Annotations
∀[C:SmallCategory]. ∀[X:ps_context{j:l}(C)]. ∀[A,B,E:{X ⊢ _}]. ∀[g:{X ⊢ _:(A ⟶ B)}]. ∀[f:{X ⊢ _:(B ⟶ E)}].
  ((f o g) ∈ {X ⊢ _:(A ⟶ E)})
BY
{ (ProveWfLemma
   THEN (InstLemma `presheaf-app_wf_fun` [⌜parm{i}⌝;⌜parm{i|j}⌝;⌜C⌝;⌜X.A⌝;⌜(A)p⌝;⌜(B)p⌝;⌜(g)p⌝;⌜q⌝]⋅ THENA Auto)
   THEN InstLemma `presheaf-app_wf_fun` [⌜parm{i}⌝;⌜parm{i|j}⌝;⌜C⌝;⌜X.A⌝;⌜(B)p⌝;⌜(E)p⌝;⌜(f)p⌝;⌜app((g)p; q)⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[X:ps\_context\{j:l\}(C)].  \mforall{}[A,B,E:\{X  \mvdash{}  \_\}].  \mforall{}[g:\{X  \mvdash{}  \_:(A  {}\mrightarrow{}  B)\}].
\mforall{}[f:\{X  \mvdash{}  \_:(B  {}\mrightarrow{}  E)\}].
    ((f  o  g)  \mmember{}  \{X  \mvdash{}  \_:(A  {}\mrightarrow{}  E)\})


By

---

Latex:
(ProveWfLemma
  THEN  (InstLemma  `presheaf-app\_wf\_fun`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}(A)p\mkleeneclose{};\mkleeneopen{}(B)p\mkleeneclose{};\mkleeneopen{}(g)p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  InstLemma  `presheaf-app\_wf\_fun`  [\mkleeneopen{}parm\{i\}\mkleeneclose{};\mkleeneopen{}parm\{i|j\}\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X.A\mkleeneclose{};\mkleeneopen{}(B)p\mkleeneclose{};\mkleeneopen{}(E)p\mkleeneclose{};\mkleeneopen{}(f)p\mkleeneclose{};
  \mkleeneopen{}app((g)p;  q)\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index