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