---

Step * 2 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 : psc_map{[i | j]:l}(C; X; discrete-set(T))
⊢ x ∈ {X ⊢ _:discr(T)}
BY
{ D -1 }

1
1. C : SmallCategory
2. T : Type
3. X : ps_context{j:l}(C)
4. x : A:cat-ob(op-cat(C)) ⟶ (cat-arrow(type-cat{[i | j]':l}) (X A) (discrete-set(T) A))
5. ∀A,B:cat-ob(op-cat(C)). ∀g:cat-arrow(op-cat(C)) A B.
     ((cat-comp(type-cat{[i | j]':l}) (X A) (discrete-set(T) A) (discrete-set(T) B) (x A) (discrete-set(T) A B g))
     = (cat-comp(type-cat{[i | j]':l}) (X A) (X B) (discrete-set(T) B) (X A B g) (x B))
     ∈ (cat-arrow(type-cat{[i | j]':l}) (X A) (discrete-set(T) B)))
⊢ x ∈ {X ⊢ _:discr(T)}

---

Latex:

---

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


By

---

Latex:
D  -1

---

Home Index