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

[Vladimir Voevodsky <vlad...@ias.edu>]

[-- Attachment #1: Type: text/plain, Size: 2133 bytes --]

Our definition of the category of elements (cf. ElementsOp.v in UniMath/UniMath/Ktheory), and I think it is the standard one, is that morphisms are morphisms f:X -> X’ such that  p=P(f)(p’). Then all works as expected.


> On Feb 24, 2017, at 10:06 AM, Paolo Capriotti <p.cap...@gmail.com> wrote:
> 
> 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
> 
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Univalent Mathematics" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to univalent-mathem...@googlegroups.com <mailto:univalent-mathem...@googlegroups.com>.
> To post to this group, send email to univalent-...@googlegroups.com <mailto:univalent-...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/univalent-mathematics <https://groups.google.com/group/univalent-mathematics>.
> To view this discussion on the web visit https://groups.google.com/d/msgid/univalent-mathematics/ebf61361-d581-4a25-98cf-0e345e2e2035%40googlegroups.com <https://groups.google.com/d/msgid/univalent-mathematics/ebf61361-d581-4a25-98cf-0e345e2e2035%40googlegroups.com?utm_medium=email&utm_source=footer>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #2: Type: text/html, Size: 3158 bytes --]