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

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

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…?

> On Feb 24, 2017, at 9:33 AM, Paolo Capriotti <pa...@capriotti.io> wrote:
> 
>>> On Feb 23, 2017, at 1:52 PM, Benedikt Ahrens <benedik...@gmail.com> wrote:
>>> Section 1.4.8 "Equality" gives an informal account and points to several
>>> precise definitions.
>>> On page 43 two equality types are considered, one intensional one and
>>> one with reflection rule.
> 
> I haven't actually considered something like what Vladimir suggested, though.  In the systems that I described in my thesis, exact equality is defined for every type.
> 
> Vladimir Voevodsky writes:
>> BTW It is a little dangerous to define presheaves as functors C -> Sets^{op}. While it gives the correct objects, the morphisms between presheaves are not morphisms in the category of functors C -> Sets^{op} but in the opposite category.
> 
> Ah, right.  The reason why I defined presheaves this way is that you can just say that the slice category over a presheaf $P$ is presheaves over the category of elements of $P$, rather than copresheaves, so it's more uniform and certain proofs become a little bit nicer.  Of course, one could start with C^{op} and use copresheaves throughout, but then I think things would get quite confusing with the Yoneda embedding.
> 
> But thanks for pointing out this problem.  Somehow, it had never occured to me that natural transformations are going in the wrong direction with my definition.
> 
> 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.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at https://groups.google.com/group/univalent-mathematics.
> To view this discussion on the web visit https://groups.google.com/d/msgid/univalent-mathematics/87k28fek09.fsf%40capriotti.io.
> For more options, visit https://groups.google.com/d/optout.