Re: [UniMath] Re: [HoTT] about the HTS

[Paolo Capriotti <p.cap...@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 877 bytes --]

Vladimir Voevodsky writes:
> The slice category over P is equivalent to presheaves on the category of 
elements of P. What is your definition of the category of elements of $P$? 
Objects are pairs $(X:C,p:P(X))$, and morphisms from $(X,p)$ to $(X’,p’)$ 
are…?

...morphisms $f : C(X',X)$ such that $Pf(p) = p'$.

The slice category of the category of functors $A -> Set$ over a functor 
$F$ is equivalent to functors $el(F) -> Set$, right?  Now if you define 
presheaves as functors $C^{op} -> Set$, you get that presheaves on $C$ over 
a presheaf $P$ are equivalent to *functors* $el(P) -> Set$, not presheaves 
on $el(P)$.

That's why I was trying to be clever and use that unnatural definition of 
presheaves, but, as you pointed out, that doesn't work either, because the 
resulting category of presheaves is the opposite of what we want.

Paolo


[-- Attachment #1.2: Type: text/html, Size: 1031 bytes --]