Timeline for Using induction to define Indexed family of HITs in agda
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 25, 2022 at 4:16 | comment | added | IsAdisplayName |
@Cactus ah, I think this is the confusion. $G(n+1)$ is not meant to be a term of type $(n+1)-glob$. Rather, I intend it to be a path as follows $G(n+1) : in(Gn) = Gn_2$. In this case, I use the shorthand of in(G(n+1)) for the higher dimensional action of paths of in on G(n+1). Anyways, learned a way to formalize this that avoids all this mess. Thank you though!
|
|
| Jul 25, 2022 at 1:44 | comment | added | Cactus |
The rhs is G(n+1)_2 : in(in(Gn)) = in(Gn_2) a path, yes. But the left-hand side is in(G(n+1)) : (n+2)-glob, a point. So your constructor G(n+2) has a type which is supposedly a path between a path and a point.
|
|
| Jul 23, 2022 at 15:34 | comment | added | IsAdisplayName | @Cactus the rhs is a path type. A point is just a term in a type. | |
| Jul 23, 2022 at 4:31 | comment | added | Cactus |
G(n+2) : in(G(n+1)) = G(n+1)_2 doesn't seem well-typed to me: the left-hand side is a point, the right-hand side is a path.
|
|
| Jun 3, 2022 at 6:33 | vote | accept | IsAdisplayName | ||
| Jun 3, 2022 at 6:33 | |||||
| Jun 3, 2022 at 6:33 | history | edited | IsAdisplayName | CC BY-SA 4.0 |
added 4 characters in body
|
| Jun 3, 2022 at 6:32 | comment | added | IsAdisplayName | @Trebor This was more complicated than I hoped. I'm probably going to end up asking my advisor about this. Thank you for the help, though! | |
| Jun 3, 2022 at 6:29 | comment | added | IsAdisplayName | oh, thats a typo. I think it should read in(in(Gn)) = in(Gn_2). I intended Gn to be the filler of the n-glob. Then, to create the n+1 glob, copy the n-glob with in and add a path Gn_2 which is parallel to in(Gn). Then, add G(n+1) : in (Gn) = Gn_2. So, in(Gn) and Gn_2 should be parallel n globs living in the type of the n+1 glob, with filler G(n+1). To create the (n+2)-glob, copy again with in. So we should have ```in(Gn+1) : in(in(Gn))=in(Gn_2). Add in a parallel path G(n+1)_2 and a filler G(n+2). | |
| Jun 3, 2022 at 4:33 | history | edited | IsAdisplayName | CC BY-SA 4.0 |
added 812 characters in body
|
| Jun 3, 2022 at 3:14 | answer | added | Trebor♦ | timeline score: 3 | |
| Jun 2, 2022 at 23:02 | history | asked | IsAdisplayName | CC BY-SA 4.0 |