---

Step * 1 1 of Lemma pscm-presheaf-lambda

.....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)
BY
{ (RepUR ``pscm+ pscm-ap pscm-adjoin psc-snd psc-adjoin-set pscm-comp psc-fst`` 0
   THEN Fold `psc-adjoin-set` 0
   THEN EqCDA) }

1
.....subterm..... T:t
1: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 I a) = (s J f(a)) ∈ X(J)

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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)
10.  J  :  cat-ob(C)
11.  f  :  cat-arrow(C)  J  I
12.  u  :  A(f((s)a))
\mvdash{}  (f((s)a);u)  =  (s+)(f(a);u)


By

---

Latex:
(RepUR  ``pscm+  pscm-ap  pscm-adjoin  psc-snd  psc-adjoin-set  pscm-comp  psc-fst``  0
  THEN  Fold  `psc-adjoin-set`  0
  THEN  EqCDA)

---

Home Index