---

Step * 1 1 of Lemma subset-presheaf-term


1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Y : ps_context{j:l}(C)
4. sub_ps_context{j:l}(C; Y; X)
5. {X ⊢ _} ⊆r {Y ⊢ _}
6. A : {X ⊢ _}
7. x : {X ⊢ _:A}
8. 1(Y) ∈ psc_map{j:l}(C; Y; X)
9. (x)1(Y) ∈ {Y ⊢ _:(A)1(Y)}
10. I : cat-ob(C)
11. a : Y(I)
⊢ ((x)1(Y) I a) = (x I a) ∈ A(a)
BY
{ (RepUR ``pscm-ap-term pscm-id pscm-ap`` 0 THEN Fold `member` 0 THEN Fold `presheaf-term-at` 0) }

1
1. C : SmallCategory
2. X : ps_context{j:l}(C)
3. Y : ps_context{j:l}(C)
4. sub_ps_context{j:l}(C; Y; X)
5. {X ⊢ _} ⊆r {Y ⊢ _}
6. A : {X ⊢ _}
7. x : {X ⊢ _:A}
8. 1(Y) ∈ psc_map{j:l}(C; Y; X)
9. (x)1(Y) ∈ {Y ⊢ _:(A)1(Y)}
10. I : cat-ob(C)
11. a : Y(I)
⊢ x(a) ∈ A(a)

---

Latex:

---

Latex:

1.  C  :  SmallCategory
2.  X  :  ps\_context\{j:l\}(C)
3.  Y  :  ps\_context\{j:l\}(C)
4.  sub\_ps\_context\{j:l\}(C;  Y;  X)
5.  \{X  \mvdash{}  \_\}  \msubseteq{}r  \{Y  \mvdash{}  \_\}
6.  A  :  \{X  \mvdash{}  \_\}
7.  x  :  \{X  \mvdash{}  \_:A\}
8.  1(Y)  \mmember{}  psc\_map\{j:l\}(C;  Y;  X)
9.  (x)1(Y)  \mmember{}  \{Y  \mvdash{}  \_:(A)1(Y)\}
10.  I  :  cat-ob(C)
11.  a  :  Y(I)
\mvdash{}  ((x)1(Y)  I  a)  =  (x  I  a)


By

---

Latex:
(RepUR  ``pscm-ap-term  pscm-id  pscm-ap``  0  THEN  Fold  `member`  0  THEN  Fold  `presheaf-term-at`  0)

---

Home Index