---

Step * 1 of Lemma pscm-adjoin-wf


1. C : SmallCategory
2. Gamma : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. A : {Gamma ⊢' _}
5. sigma : psc_map{j:l}(C; Delta; Gamma)
6. u : {Delta ⊢ _:(A)sigma}
7. I : cat-ob(C)
8. J : cat-ob(C)
9. g : cat-arrow(C) J I
⊢ (λs.g(<(sigma)s, u I s>)) = (λs.<(sigma)g(s), u J g(s)>) ∈ (Delta(I) ⟶ Gamma.A(J))
BY
{ (Fold `psc-adjoin-set` 0 THEN EqCDA) }

1
.....subterm..... T:t
1:n
1. C : SmallCategory
2. Gamma : ps_context{j:l}(C)
3. Delta : ps_context{j:l}(C)
4. A : {Gamma ⊢' _}
5. sigma : psc_map{j:l}(C; Delta; Gamma)
6. u : {Delta ⊢ _:(A)sigma}
7. I : cat-ob(C)
8. J : cat-ob(C)
9. g : cat-arrow(C) J I
10. s : Delta(I)
⊢ g(((sigma)s;u I s)) = ((sigma)g(s);u J g(s)) ∈ Gamma.A(J)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  Gamma  :  ps\_context\{j:l\}(C)
3.  Delta  :  ps\_context\{j:l\}(C)
4.  A  :  \{Gamma  \mvdash{}'  \_\}
5.  sigma  :  psc\_map\{j:l\}(C;  Delta;  Gamma)
6.  u  :  \{Delta  \mvdash{}  \_:(A)sigma\}
7.  I  :  cat-ob(C)
8.  J  :  cat-ob(C)
9.  g  :  cat-arrow(C)  J  I
\mvdash{}  (\mlambda{}s.g(<(sigma)s,  u  I  s>))  =  (\mlambda{}s.<(sigma)g(s),  u  J  g(s)>)


By

---

Latex:
(Fold  `psc-adjoin-set`  0  THEN  EqCDA)

---

Home Index