Step * of Lemma presheaf-cumulativity1

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

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

2
.....eq aux..... 
1. 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