---

Step * 1 of Lemma discrete-presheaf-term-is-map

.....subterm..... T:t
1:n
1. C : SmallCategory
2. T : Type
3. X : ps_context{j:l}(C)
4. x : {X ⊢ _:discr(T)}
⊢ x ∈ psc_map{[i | j]:l}(C; X; discrete-set(T))
BY
{ D -1 }

1
1. C : SmallCategory
2. T : Type
3. X : ps_context{j:l}(C)
4. x : I:cat-ob(C) ⟶ a:X(I) ⟶ discr(T)(a)
5. ∀I,J:cat-ob(C). ∀f:cat-arrow(C) J I. ∀a:X(I).  ((x I a a f) = (x J f(a)) ∈ discr(T)(f(a)))
⊢ x ∈ psc_map{[i | j]:l}(C; X; discrete-set(T))

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  C  :  SmallCategory
2.  T  :  Type
3.  X  :  ps\_context\{j:l\}(C)
4.  x  :  \{X  \mvdash{}  \_:discr(T)\}
\mvdash{}  x  \mmember{}  psc\_map\{[i  |  j]:l\}(C;  X;  discrete-set(T))


By

---

Latex:
D  -1

---

Home Index