Cale 2017-02-25 23:45:20
bollu: right?
bollu 2017-02-25 23:45:26
Cale: yes
Cale 2017-02-25 23:46:29
bollu: So, now those (up to homotopy equivalence) become the horizontal and vertical composition from the abstract version of the Eckmann Hilton argument you might've seen
bollu 2017-02-25 23:46:43
Cale: ahh
bollu 2017-02-25 23:46:45
Cale: interesting
Cale 2017-02-25 23:47:25
and basically, the commutativity will amount to the fact that you can ultimately just rotate your sphere
bollu 2017-02-25 23:47:44
to realign things I'm guessing?
Cale 2017-02-25 23:49:24
Well, it's not quite the same as just rotating, because that would result in the two halves being "backward"
bollu 2017-02-25 23:57:55
hm, I do not know fibrations from topology very well
Cale 2017-02-25 23:57:57
Pi (x:A), T x is the space of sections
bollu 2017-02-25 23:58:00
I suppose I'll have to go and study that first
Cale 2017-02-25 23:58:25
ah, I assumed you did, because of the way you asked the question :)
bollu 2017-02-25 23:58:33
Cale: no :)
bollu 2017-02-25 23:58:59
Cale: eh, I know very little algebraic topology (I've seen some homotopy and some simplicial homology), will that be enough?
bollu 2017-02-25 23:59:03
or do I just "move on"?
Cale 2017-02-25 23:59:16
Should be
bollu 2017-02-25 23:59:25
Cale: OK, cool
bollu 2017-02-25 23:59:34
Cale: thanks!
Cale 2017-02-26 00:02:33
If you've never come across the homotopy lifting property before, and you want to understand that in detail, that'll take a little bit of work, but it doesn't have much in the way of dependencies.
bollu 2017-02-26 00:02:33
Cale: I see, OK
bollu 2017-02-26 00:02:33
Cale: is it in any way related to path lifting?
bollu 2017-02-26 00:02:33
Cale: over the universal cover?
Aku 2017-02-26 00:05:53
bollu : Can you just take a look!
Cale 2017-02-26 00:09:00
Yeah, the universal cover is a special example of a fibration.
Aku 2017-02-26 00:09:01
I have written
Aku 2017-02-26 00:09:01
it
bollu 2017-02-26 00:09:02
Aku: yep, I told you the types that it should have
bollu 2017-02-26 00:09:07
Aku: what else is confusing :)
Aku 2017-02-26 00:10:03
but I had to write pDefn :: Parser(String,Expr Name)
Aku 2017-02-26 00:11:37
instead of Parser(String,Expr a)'
Aku 2017-02-26 00:12:24
I will paste it!
lpaste_ 2017-02-26 00:12:24
Aku revised "figuring out type?": "figuring out type?" at http://lpaste.net/7251168297717071872
bollu 2017-02-26 00:12:24
Aku: also note that Expr a == CoreExpr
Aku 2017-02-26 00:12:24
Nopes
Aku 2017-02-26 00:12:24
CoreExpr == Expr Name
Aku 2017-02-26 00:12:24
Name::String
bollu 2017-02-26 00:12:24
Aku: oh yes, I meant Expr Name* sorry :)
bollu 2017-02-26 00:12:24
yeah so
bollu 2017-02-26 00:12:24
first of all
Aku 2017-02-26 00:12:24
yes?
bollu 2017-02-26 00:12:24
yeah, you know what pDefn has to be right
bollu 2017-02-26 00:12:24
you know what information you want to keep from the definition syntax
bollu 2017-02-26 00:12:24
the "=" is pointless
Aku 2017-02-26 00:12:24
Ya right
bollu 2017-02-26 00:12:24
you just care about the LHS name and the RHS expression
bollu 2017-02-26 00:12:24
so I would suggest
bollu 2017-02-26 00:12:24
perhaps make a data type
Aku 2017-02-26 00:12:24
That's how I defined foo3
Aku 2017-02-26 00:14:09
bollu: Its working fine
Aku 2017-02-26 00:14:15
Just one thing
bollu 2017-02-26 00:14:33
Aku: yes?
Aku 2017-02-26 00:14:43
After it parses, it reaches "in" and then parses (pExpr)
Aku 2017-02-26 00:14:56
but it retains whatever is parsed
Aku 2017-02-26 00:15:00
as unparsed tokens
Aku 2017-02-26 00:15:32
Where is it going wrong?
Aku 2017-02-26 00:15:50
I think my pExpr is incomplete!
bollu 2017-02-26 00:15:56
Aku: what do you mean?
bollu 2017-02-26 00:16:05
Aku: remember that it returns the list of all _possible_ parses
Aku 2017-02-26 00:16:24
Ya right
Aku 2017-02-26 00:16:40
Suppose I write let x = 3 in y
bollu 2017-02-26 00:16:42
yes
Aku 2017-02-26 00:16:51
It gives me y as unparsed token
Aku 2017-02-26 00:16:56
That's it
Aku 2017-02-26 00:17:19
As the first parse
Aku 2017-02-26 00:35:53
Ohh..it's monadic, is it, I will study it quite soon
