---

Step * of Lemma presheaf-cumulativity1

No Annotations
∀[C:SmallCategory]. (presheaf{j:l}(C) ⊆r presheaf{[i | j]:l}(C))
BY
{ (Auto THEN D 0) }

1
.....subterm..... T:t
1:n
1. C : SmallCategory
2. x : presheaf{j:l}(C)
⊢ x ∈ presheaf{[i | j]:l}(C)

2
.....eq aux..... 
1. C : SmallCategory
⊢ istype(presheaf{j:l}(C))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[C:SmallCategory].  (presheaf\{j:l\}(C)  \msubseteq{}r  presheaf\{[i  |  j]:l\}(C))


By

---

Latex:
(Auto  THEN  D  0)

---

Home Index