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