---

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

No Annotations
∀[C:SmallCategory]. ∀[T:Type]. ∀[X:ps_context{j:l}(C)].  {X ⊢ _:discr(T)} ≡ psc_map{[i | j]:l}(C; X; discrete-set(T))
BY
{ (Auto THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
.....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))

2
.....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)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  \mforall{}[T:Type].  \mforall{}[X:ps\_context\{j:l\}(C)].
    \{X  \mvdash{}  \_:discr(T)\}  \mequiv{}  psc\_map\{[i  |  j]:l\}(C;  X;  discrete-set(T))


By

---

Latex:
(Auto  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index