---

Step * 1 of Lemma pscm-presheaf-lambda


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : {X.A ⊢ _:B}
6. H : ps_context{j:l}(C)
7. s : psc_map{j:l}(C; H; X)
8. I : cat-ob(C)
9. a : H(I)
⊢ (λb)((s)a) = (λ(b)s+)(a) ∈ (J:cat-ob(C) ⟶ f:(cat-arrow(C) J I) ⟶ u:A(f((s)a)) ⟶ B((f((s)a);u)))
BY
{ (RepeatFor 3 ((FunExt THENA Auto))
   THEN RepUR ``presheaf-lambda presheaf-term-at`` 0
   THEN Fold `presheaf-term-at` 0
   THEN (RWO  "pscm-ap-term-at" 0 THENA Auto)
   THEN EqCDA) }

1
.....subterm..... T:t
3:n
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. A : {X ⊢ _}
4. B : {X.A ⊢ _}
5. b : {X.A ⊢ _:B}
6. H : ps_context{j:l}(C)
7. s : psc_map{j:l}(C; H; X)
8. I : cat-ob(C)
9. a : H(I)
10. J : cat-ob(C)
11. f : cat-arrow(C) J I
12. u : A(f((s)a))
⊢ (f((s)a);u) = (s+)(f(a);u) ∈ X.A(J)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  A  :  \{X  \mvdash{}  \_\}
4.  B  :  \{X.A  \mvdash{}  \_\}
5.  b  :  \{X.A  \mvdash{}  \_:B\}
6.  H  :  ps\_context\{j:l\}(C)
7.  s  :  psc\_map\{j:l\}(C;  H;  X)
8.  I  :  cat-ob(C)
9.  a  :  H(I)
\mvdash{}  (\mlambda{}b)((s)a)  =  (\mlambda{}(b)s+)(a)


By

---

Latex:
(RepeatFor  3  ((FunExt  THENA  Auto))
  THEN  RepUR  ``presheaf-lambda  presheaf-term-at``  0
  THEN  Fold  `presheaf-term-at`  0
  THEN  (RWO    "pscm-ap-term-at"  0  THENA  Auto)
  THEN  EqCDA)

---

Home Index