---

Step * 1 2 of Lemma presheaf-fun-as-presheaf-pi

.....subterm..... T:t
2:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X ⊢ _}
⊢ (λI,J,f,a,w,K,g. (w K (cat-comp(C) K J I g f)))
= (λI,J,f,a,w,K,g. (w K (cat-comp(C) K J I g f)))
∈ (I:cat-ob(C)
  ⟶ J:cat-ob(C)
  ⟶ f:(cat-arrow(C) J I)
  ⟶ a:X(I)
  ⟶ ((λI,a. presheaf-fun-family(C; X; A; B; I; a)) I a)
  ⟶ ((λI,a. presheaf-fun-family(C; X; A; B; I; a)) J f(a)))
BY
{ (Fold `member` 0
   THEN Reduce 0
   THEN Auto
   THEN InstLemma `presheaf-fun-family-comp` [⌜C⌝;⌜X⌝;⌜X⌝;⌜1(X)⌝;⌜I⌝;⌜J⌝;⌜f⌝;⌜a⌝;⌜A⌝;⌜B⌝;⌜w⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X  \mvdash{}  \_\}
\mvdash{}  (\mlambda{}I,J,f,a,w,K,g.  (w  K  (cat-comp(C)  K  J  I  g  f)))  =  (\mlambda{}I,J,f,a,w,K,g.  (w  K  (cat-comp(C)  K  J  I  g  f)))


By

---

Latex:
(Fold  `member`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  InstLemma  `presheaf-fun-family-comp`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}1(X)\mkleeneclose{};\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}J\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index