---

Step * 1 1 of Lemma pscm-adjoin-wf

.....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)
BY
{ (Assert (u I s (sigma)s g) = (u J g(s)) ∈ A(g((sigma)s)) BY
         (Fold `presheaf-term-at` 0
          THEN (RWO "presheaf-term-at-morph<" 0 THENA Auto)
          THEN RWO "pscm-presheaf-type-ap-morph" 0
          THEN Auto)) }

1
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)
11. (u I s (sigma)s g) = (u J g(s)) ∈ A(g((sigma)s))
⊢ g(((sigma)s;u I s)) = ((sigma)g(s);u J g(s)) ∈ Gamma.A(J)

---

Latex:

---

Latex:
.....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  \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
10.  s  :  Delta(I)
\mvdash{}  g(((sigma)s;u  I  s))  =  ((sigma)g(s);u  J  g(s))


By

---

Latex:
(Assert  (u  I  s  (sigma)s  g)  =  (u  J  g(s))  BY
              (Fold  `presheaf-term-at`  0
                THEN  (RWO  "presheaf-term-at-morph<"  0  THENA  Auto)
                THEN  RWO  "pscm-presheaf-type-ap-morph"  0
                THEN  Auto))

---

Home Index