---

Step * 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)}
⊢ (x)1(Y) = x ∈ {Y ⊢ _:A}
BY
{ (PresheafTermEqual THENA Auto) }

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)1(Y) I a) = (x I 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)\}
\mvdash{}  (x)1(Y)  =  x


By

---

Latex:
(PresheafTermEqual  THENA  Auto)

---

Home Index