Confusion about Definition 8.6.5, page 286
47 views
Skip to first unread message
Yiming Xu
Mar 17, 2019, 6:10:29 AM3/17/19
to HoTT Cafe
On the begining of page 286, the book writes the dependent path $code(N) = ^{\lambda y. (N = y)\mapsto U_{merid(x_1)}}code(S)$ translates to a family of paths 2.9.6. But I looked up 2.9.6 and cannot get there and ended up with messing up the calculation. I tried reversing the path $merid(x_1)$, but cannot find a way to make it appear only in one side of the equation. Any help with this point, please? I understand it is hard to type up equations, if someone could just tell me what are taken to be plugged into 2.9.6 I would very appreciate.
Michael Shulman
Mar 18, 2019, 6:52:09 PM3/18/19
to Yiming Xu, HoTT Cafe
The reason it disappears from the other side of the equation is that
the target of the function types, namely the universe U, is a constant
type family, so you can use Lemma 2.3.5.
By the way, it's more portable not to refer to page numbers in the
book, since the various versions (printed, letter, a4, ebook, etc.)
have different paginations. In this case you could say "in the second
displayed equation in the proof of Definition 8.6.5".
On Sun, Mar 17, 2019 at 3:10 AM Yiming Xu <u594...@gmail.com> wrote:
>
> On the begining of page 286, the book writes the dependent path $code(N) = ^{\lambda y. (N = y)\mapsto U_{merid(x_1)}}code(S)$ translates to a family of paths 2.9.6. But I looked up 2.9.6 and cannot get there and ended up with messing up the calculation. I tried reversing the path $merid(x_1)$, but cannot find a way to make it appear only in one side of the equation. Any help with this point, please? I understand it is hard to type up equations, if someone could just tell me what are taken to be plugged into 2.9.6 I would very appreciate.
>
>
> --
> You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
the target of the function types, namely the universe U, is a constant
type family, so you can use Lemma 2.3.5.
By the way, it's more portable not to refer to page numbers in the
book, since the various versions (printed, letter, a4, ebook, etc.)
have different paginations. In this case you could say "in the second
displayed equation in the proof of Definition 8.6.5".
On Sun, Mar 17, 2019 at 3:10 AM Yiming Xu <u594...@gmail.com> wrote:
>
> On the begining of page 286, the book writes the dependent path $code(N) = ^{\lambda y. (N = y)\mapsto U_{merid(x_1)}}code(S)$ translates to a family of paths 2.9.6. But I looked up 2.9.6 and cannot get there and ended up with messing up the calculation. I tried reversing the path $merid(x_1)$, but cannot find a way to make it appear only in one side of the equation. Any help with this point, please? I understand it is hard to type up equations, if someone could just tell me what are taken to be plugged into 2.9.6 I would very appreciate.
>
>
> You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
Reply all
Reply to author
Forward
0 new messages