00:00:04 hm, maybe this paper from 1917 will enlighten me!! 00:00:08 whoever started writing about nerves being unable to cross 00:00:27 what are they getting into 00:00:59 mnoqy: hey what's that book on foundations or whatever that's under git 00:01:16 the homotopy type theory one? 00:01:19 yeah that thanks 00:01:33 http://homotopytypetheory.org/book/ this one 00:02:27 googling "hott book" gets you pinups 00:02:27 should have expected that tbh 00:03:32 does anyone actually know what it has to do with homotopy 00:03:40 no 00:05:54 they talk about it in the book 00:06:06 i don't think i'd be able to explain it though 00:06:26 i remember paths were involved but i don't remember that helping 00:06:31 -!- shikhin_ has changed nick to shikhin. 00:11:58 -!- Sgeo has joined. 00:30:42 -!- Sprocklem has quit (Ping timeout: 240 seconds). 00:34:24 > fix $ (1:).tail.(<**>[id,succ]) 00:34:25 [1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,... 00:34:29 kmc: ^ 00:34:33 nice 00:34:48 :t (<**>[id,succ]) 00:34:49 Enum b => [b] -> [b] 00:34:55 > (<**>[id,succ]) "hello" 00:34:56 "hieflmlmop" 00:35:21 oh interleaved, interesting 00:35:30 > (<**>[id,succ]) [0,1,1,2] 00:35:31 :t (<**>) 00:35:32 [0,1,1,2,1,2,2,3] 00:35:32 Applicative f => f a -> f (a -> b) -> f b 00:36:17 huh so you can get this sequence by repeatedly concat'ing the succ'd sequence OR by repeatedly interleaving the succ'd sequence 00:36:20 that's interesting 00:39:29 > fix $ (False:).tail.(<**>[id,not]) 00:39:30 [False,True,True,False,True,False,False,True,True,False,False,True,False,Tr... 00:42:41 kmc: it's basically the difference between counting bits in little-endian or big-endian order 00:43:23 oerjan: hm, yeah 00:43:48 oerjan: how would you do it with concat? 00:43:52 nooodl: yeah that's thue-morse, which is just the (inversed) parity of kmc's sequence 00:44:03 -!- Phantom_Hoover has quit (Remote host closed the connection). 00:44:25 oh hm... 00:45:57 -!- mnoqy has quit (Quit: hello). 00:45:58 oh wait kmc _did_ start his sequence at 0, it was Bike who changed that to 1. so scratch "(inversed)" 00:46:07 what 00:46:22 oh,i was just testing initial conditions. 00:46:40 > fix $ ([4,6,3]++).tail.(<**>[id,succ]) 00:46:44 can't find file: L.hs 00:46:47 > fix $ ([4,6,3]++).tail.(<**>[id,succ]) 00:46:50 [4,6,3,5,6,7,3,4,5,6,6,7,7,8,3,4,4,5,5,6,6,7,6,7,7,8,7,8,8,9,3,4,4,5,4,5,5,... 00:47:01 > (!!4) $ iterate (\x -> x ++ [map succ $ concat x]) [[0]] 00:47:02 [[0],[1],[1,2],[1,2,2,3],[1,2,2,3,2,3,3,4]] 00:47:07 that's... is that the same 00:47:21 Bike: your adjustment makes no sense with my method. 00:47:47 pshaw, expecting i'd at all understand something before hitting it with a tastefully tasseled wrench. 00:48:25 I want a function that takes a list and gives you the result of infinite iterations of (\xs -> xs ++ (map (1+) xs)). 00:48:31 > concat $ fix $ ([0]:).(\x -> x ++ [map succ $ concat x]) 00:48:32 [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,... 00:48:35 or generalize that, who fuckin cares. 00:48:39 fuck everything. fuck everybody 00:48:43 oops. fuck everything 00:48:54 I'm ahead of the curve, thefuc-related curve 00:50:04 in other words, a fixed point combinator that doesn't give bottom all the fucking time. 00:50:15 [sex joke]. 00:50:18 Bike: take the diagonal of "iterate (\xs -> xs ++ (map (1+) xs)) start". imo optimized?? 00:50:38 for speed 00:50:45 that's gotta be like O(2^n^n^n) 00:50:48 fucking 00:51:10 now let me take a few minutes to work out how to write diagnoal :V 00:51:37 zipWith (!!) xs [0..] 00:51:56 does that work?? i'm pretty tired 00:52:10 :t head 00:52:11 [a] -> a 00:52:16 > zipWith (!!) [[1,2,3],[4,5,6],[7,8,9]] [0..] 00:52:17 [1,5,9] 00:52:22 B) 00:52:23 > let f l = (+) <$> l <*> (fix $ (0:).tail.(<**>[id,succ])) in f [4,6,3] 00:52:24 [4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8,5,6,6,7,6,7,7,8,6,7,7,8,7,8,8,9,5,6,6,7,6,... 00:52:34 hm oh wait 00:53:03 > let f l = (+) <$> (fix $ (0:).tail.(<**>[id,succ])) <*> l in f [4,6,3] 00:53:05 [4,6,3,5,7,4,5,7,4,6,8,5,5,7,4,6,8,5,6,8,5,7,9,6,5,7,4,6,8,5,6,8,5,7,9,6,6,... 00:53:11 there you go >:) 00:53:16 elegant 00:53:55 > let xs = [4,6,3] ++ map (1+) xs in xs 00:53:56 [4,6,3,5,7,4,6,8,5,7,9,6,8,10,7,9,11,8,10,12,9,11,13,10,12,14,11,13,15,12,1... 00:54:09 ah. yes. ok i really need to go to bed 00:54:19 > fix (\f get xss -> (get.head xss):(f (get.tail) (tail xss))) head [[1,2,3],[4,5,6],[7,8.9]] 00:54:20 Couldn't match expected type `a0 -> [c0]' with actual type `[t0]'Couldn't m... 00:54:28 it's cool how i'm the worst programmer ever. 00:55:22 > zipWith (!!) ((\xs -> xs ++ (map succ xs)) [0]) [0..] 00:55:23 No instance for (GHC.Show.Show c0) 00:55:23 arising from a use of `M1104756188.sh... 00:55:38 ((\xs -> xs ++ (map succ xs)) [0]) 00:55:42 > ((\xs -> xs ++ (map succ xs)) [0]) 00:55:43 [0,1] 00:55:44 at least i'm a worse biologist! 00:55:53 oh, um. 00:55:57 > (iterate (\xs -> xs ++ (map succ xs)) [0]) 00:55:58 [[0],[0,1],[0,1,1,2],[0,1,1,2,1,2,2,3],[0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4],[0... 00:56:01 right. yeah. wow. 00:56:10 > zipWith (!!) (iterate (\xs -> xs ++ (map succ xs)) [0]) [0..] 00:56:12 [0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,... 00:56:36 @let diagonal ls = zipWith (!!) ls [0..] 00:56:37 Defined. 00:56:48 > diagonal $ iterate (\xs -> xs ++ (map succ xs)) [0..] 00:56:52 [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,... 00:57:00 imo i'm a genius ;_; 00:57:17 looks familiar. 00:57:24 let's check oeis 00:57:28 @oeis 0,1,2,3,4,5,6 00:57:37 Digital sum (i.e. sum of digits) of n; also called digsum(n).[0,1,2,3,4,5,6,... 00:57:43 ah yes 00:57:46 right, right. 00:57:48 the digital sum. 00:57:53 clearly. 00:57:56 digital bath 00:58:00 `thanks oeis 00:58:01 Thanks, oeis. Thoeis. 00:58:09 I dig sums 00:58:49 oeis should sort by kolmogorov complexity to avoid this sort of thing 00:58:55 > diagonal [[1,2],[3,4]] 00:58:59 [1,4] 00:59:16 ok what did i... oh, well, wow. 00:59:21 > diagonal $ iterate (\xs -> xs ++ (map succ xs)) [0] 00:59:25 [0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,... 00:59:25 yeah, ok, go me. 01:00:17 According to Oleg, zippers are delimited continuations. Not entirely sure what that means, but I wonder what implications there are for lenses 01:00:45 i wonder what implications there are for uzbekistan's human rights situation. 01:01:51 > concat . fix $ ([0]:) . map (map succ . concat) . tail . inits 01:01:52 [0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,... 01:02:18 someone asked about using concat. 01:02:28 not exactly what i had in mind, but whatever. 01:02:47 > concat . fix (([8,0,3]:) . map (map succ . concat) . tail . inits) 01:02:49 Couldn't match type `[[t0]]' with `a0 -> [[a1]]' 01:02:49 Expected type: [[t0]] -> ... 01:03:20 i recommend keeping the $ 01:03:28 > concat . fix $ ([8,0,3]:) . map (map succ . concat) . tail . inits 01:03:29 [8,0,3,9,1,4,9,1,4,10,2,5,9,1,4,10,2,5,10,2,5,11,3,6,9,1,4,10,2,5,10,2,5,11... 01:03:39 ah this one works. Good Job 01:04:02 > concat . fix $ ([8,0,3]:) . map (tail . concat) . tail . inits 01:04:03 [8,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,0,3,... 01:04:09 cool 01:04:57 oh wait hm... 01:06:08 -!- nooodl has quit (Ping timeout: 268 seconds). 01:06:14 > concat . fix $ ([0]:) . scanl (++) . map (map succ) 01:06:15 Couldn't match type `[[[b0]]] -> [[[b0]]]' with `[[b0]]' 01:06:15 Expected type: [[... 01:06:49 :t scanl 01:06:50 (a -> b -> a) -> a -> [b] -> [a] 01:07:05 > concat . fix $ ([0]:) . scanl1 (++) . map (map succ) 01:07:07 [0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,... 01:07:59 less duplication of work 01:08:09 highly efficient 01:17:07 http://da-data.blogspot.kr/2013/03/optimistic-cuckoo-hashing-for.html 01:22:23 -!- conehead has quit (Ping timeout: 272 seconds). 01:26:16 -!- Sprocklem has joined. 01:31:43 -!- Halite has quit (Ping timeout: 250 seconds). 01:45:56 -!- Sprocklem has quit (Read error: Connection reset by peer). 01:46:11 -!- Sprocklem has joined. 01:55:09 -!- Halite[tired] has joined. 01:57:12 "Now the secret can be revealed: IO is a monad. Being a monad means you have access to some syntactical sugar with the do notation." 01:57:14 what did I say 02:00:53 time to write your monad tutorial "Monads are like what did I say" 02:04:06 what is with wikipedia's "george" theme 02:04:49 -!- doesthiswork has joined. 02:12:31 ok https://en.wikipedia.org/wiki/Wikipedia_talk:Today%27s_featured_article#The_week_of_George.3F 02:12:44 i recall the Eagles, too. 02:16:52 finally girl genius updated 02:17:13 giant statues of agatha: check 02:25:11 -!- shikhin has quit (Ping timeout: 272 seconds). 02:26:15 Is Dream a Little Dream a good episode? 02:28:37 I wonder why they build the giant agatha statues 02:30:29 doesthiswork: i think gil got a little crazier in the time that has passed 02:31:10 he's _really_ obsessing about her now. 02:31:22 I wonder if he really is infected 02:31:31 or maybe he's a clone 02:31:41 and the real gil is still locked up 02:32:08 well old klaus said he had used a different form of mind control on him, which would mean he is _not_ wasp infected 02:32:17 assuming that was true. 02:32:20 or wait 02:33:06 klaus also made it _look_ like gil is infected, but that was clearly fake, because the weasel critter did not react to _klaus_ and we _know_ he is infected. 02:33:39 -!- Koen_ has quit (Quit: Koen_). 02:33:49 that's my reasoning, anyway. 02:34:19 but with all the Other clones running around, who knows what has happened in the meantime. 02:36:20 also at the time that happened, there hadn't been time enough to make a new spark-infecting wasp, i assume. presumably there will have been now, so he could have been infected later. 02:37:13 otoh with the empire collapsed the Other might not really care what gil does any more. 02:37:54 any way i was just satisfied that my guess last week that there would be giant statues was correct :) 02:38:31 also i'm monologuing, which means it's time for... 02:38:37 *MWAHAHAHAHAHAHAHAHAHAHAHAHA* 02:41:33 -!- FreeFull has quit (Ping timeout: 272 seconds). 02:43:47 -!- FreeFull has joined. 02:59:53 -!- fishduck has joined. 03:26:37 -!- fishduck has left. 03:31:34 -!- shachaf has joined. 03:31:49 kmc: There, it's clearly on-topic here. 03:40:17 is hashing that esoteric? 03:43:47 yes 04:02:40 perhaps hash will fix etc. 04:09:40 -!- CADD has joined. 04:10:04 -!- CADD has changed nick to Guest41528. 04:10:17 kmc: so when you do new Foo[n] and Foo is a POD type gcc won't store n 04:10:41 sensible 04:10:48 can you do that with templates in a reasonable way 04:11:19 -!- kmc has set topic: ewige blumenkraft | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf | logs: http://codu.org/logs/_esoteric/ or http://tunes.org/~nef/logs/esoteric/. 04:12:01 with http://www.cplusplus.com/reference/type_traits/is_pod/ i imagine 04:14:13 oh is that new 04:16:04 Boost has had them for a while 04:38:31 -!- shikhin has joined. 04:39:11 -!- oerjan has quit (Quit: leaving). 04:43:16 -!- shikhin_ has joined. 04:44:28 -!- Guest41528 has quit (Remote host closed the connection). 04:46:23 -!- shikhin has quit (Ping timeout: 260 seconds). 04:47:13 -!- Sprocklem has quit (Ping timeout: 246 seconds). 05:04:22 http://www.bbc.co.uk/news/blogs-news-from-elsewhere-24707337 "Russia: Hidden chips 'launch spam attacks from irons'" 05:10:10 How do I generalize a shifting pattern ((0,1,2,3,4,5,6,7,8,9,a,b,c,d,e,f) then (1,2,3,4,5,6,7,8,9,a,b,c,d,e,f,0)) in a ROM to any number of address and/or data bits? 05:10:55 huh? 05:11:18 I'm talking about ROMs and patterns in their data 05:11:23 okay 05:11:35 generally the patterns in a ROM aren't represented specially 05:11:56 afaik 05:12:00 How do I generalize it so I can calculate the pattern for 64 address bits and 32 data bits? 05:12:02 you just have a pile of bits 05:12:07 what pattern? 05:12:14 The pattern I said 05:12:32 what does that pattern have to do with ROMs? 05:12:58 well I have a ROM containing one for 8 address bits and 4 data bits in Logisim. 05:13:11 How do I generalize it? 05:13:26 So I can put it for 64 address/32 data? 05:32:42 -!- trout has changed nick to const. 05:36:35 " kmc: now stuck thinking of analogies between dynamic systems and iterated functions. V_V" an iterated function system can be thought of as a dynamical system, the functions giving an action of the free monoid 05:36:47 your mom's a free monoid 05:36:56 the fixed-point they generate is the limit set of the system 05:37:35 (fixed-points are what you care about for IFS, and limit sets are something you care about for dynamical systems) 05:37:57 aren't they the same thing 05:38:02 wait you just said that 05:38:59 was halite asking how to make a shifter 05:41:23 -!- asie has joined. 05:42:17 i thought about linking http://en.wikipedia.org/wiki/Barrel_shifter but wasn't sure if it was relevant 05:42:20 but that's a thing 05:42:26 don't know what it has to do with ROMs though 05:42:47 there's always a tradeoff between storing your lookup table in ROM vs. computing it with gates 05:45:29 What's with people magically introducing GADT syntax just to express a type like "data T a = C a => T a"? 05:45:37 GADT syntax is the best, is what 05:45:51 in my hypothetical Haskell tutorial i will never get around to writing, we will use GADT syntax from the beginning 05:46:06 OK, then use it uniformly. 05:46:06 it's less confusing 05:46:10 yes, one should 05:46:20 "The basic results on this resonance were obtained not by strict mathematical arguments but by a combination of guesses and computer experiments" 05:46:27 when you write «data Foo = Bar» it's super confusing that Foo is a type and Bar a value cause there's an equals sign between them!! 05:46:30 should be a kind error imo 05:46:36 But writing "don't do data C a => T a = T a, because blah blah, instead you should do data T a where T :: C a => a -> T a" 05:46:49 That's introducing two unrelated things at once 05:46:56 sure, but the former is almost never useful 05:47:12 you're saying you can write «data T a = C a => T a» in GHC? 05:47:15 and get the latter behavior? 05:47:18 Yes. 05:47:20 hm 05:47:25 that's pretty obscure though, isn't it? 05:47:30 and again, GADT syntax is clearer 05:47:39 Bike: several layers of Halachic uncertainty, randomness, and delays 05:47:44 Is it? It seems pretty obvious to me if that's the behavior you're oging for. 05:47:48 shrug 05:47:58 It's as obscure as ExistentialQuantification. 05:48:19 i'm already streaming through the weird russian names here, if you told me jews came up with this four thousand years ago i'd belive you (because of knuth THANKS KNUTH) 05:48:38 Anyway, every GADT is represented in GHC using a combination of ExistentialQuantification and various constraints like this (including type equality constraints). 05:49:00 sure 05:49:08 Anyway I don't object to either syntax, just to jumping to GADTs for no good reason. 05:49:13 i feel i'm worryingly close to learning what homotopy really is. 05:49:17 I found the syntax very confusing when I first saw it. 05:49:19 But anyway. 05:50:03 The trouble with GADT syntax is that it's verbose. 05:51:16 Bike: what's homotopy 05:51:30 a functor on the category of curves, 05:51:40 endofunctor. whtever, fuck other functors. 05:51:59 what's that category 05:52:02 Bike: http://languagelog.ldc.upenn.edu/myl/llog/Gan11.jpg 05:52:33 a strong argument against socialist price regulation 05:53:30 what's a curve and what's a curve homomorphism 05:53:36 i think a homotopy is just a continuous function between continuous functions, though. 05:54:01 no, wait, no, it's more like parametrized. 05:54:05 w/e. i don't know shit. 05:54:38 a curve is something with a homotopy with a line segment, hth 05:55:03 am i going to have to ask https:wikipedia 05:55:35 wikipedia literally says "a topological space which is locally homeomorphic to a line" 05:56:08 holy shit there are some awesome names on wikipedia's "list of curves" 05:56:19 "Trisectrix of Maclaurin" "Tschirnhausen cubic" "Witch of Agnesi" 05:56:42 i'm pretty sure you can hire trisectrixes at brothels 05:56:47 trisectrices? 05:56:58 everyone's heard of the witch of agnesi 05:58:49 Bike: ok let's start with what's a continuous function :'( 05:59:11 do you want me to go through epsilon delta also how serious are you being 05:59:35 i mean in general for arbitrary topological spaces 05:59:44 or does some epsilon delta thing work there too 05:59:55 -!- ^v has quit (Quit: Ping timeout: 1337 seconds). 05:59:58 well as long as you have a metric, sure 06:00:32 but you don't 06:00:50 oh, yeah, what am i thinking, you don't need metrics. 06:01:05 help 06:01:20 how does the epsilon delta thing work in that case 06:01:57 " i think a homotopy is just a continuous function between continuous functions, though." a homotopy is a _path_ between two continuous functions (it's a path pointwise, and it's continuous as a whole) 06:02:14 -!- doesthiswork has quit (Quit: Leaving.). 06:02:18 something like, for f : A -> B, if you have x there must be a neighborhood of x and a neighborhood of f(x) such that all points in the first neighborhood are in the second neighborhood under f 06:02:22 i think that's wrong 06:02:49 so you move f(x) to g(x) for all x simultaneously (f and g have to have the same domain and codomain for this to make sense) 06:02:54 "f is continuous at some point x ∈ X if and only if for any neighborhood V of f(x), there is a neighborhood U of x such that f(U) ⊆ V" 06:02:59 son of a shit 06:03:13 oh, right, i just used the wrong quantifiers. 06:03:49 no that's right 06:03:51 i think that's reasonably intuitive though. 06:04:03 oh you mean at first 06:04:04 the thing i quoted is right because i didn't write it. the one i did write is wrong :D 06:04:09 ok 06:04:33 this is where the whole "bike actually hasn't taken math past calculus" thing comes into play 06:04:42 btw i don't know any maths at all 06:04:50 shachaf: does the definition make sense? 06:05:40 (generally people learn continuity quite a bit before homotopy) 06:06:11 this is #esoteric, we don't give a shit about your "coherent pedagogical methods"!! 06:06:27 with your first definition, every function is continuous 06:06:37 right, very wrong 06:06:42 so yeah that's probably not right 06:06:44 Bike: yes 06:06:49 good 06:07:42 since you could just take the neighborhood that is the entire space on both ends, which i realized while writing it, but i kept going anyway because gosh darn it sounded almost right. 06:08:09 yeah 06:08:15 but of course if it's that every neighborhood of f has to have an image, you can keep shrinking that shit. which matches the intuition of continuity. 06:08:48 exactly 06:08:54 There's probably a good definition of homotopy for function spaces instead of sequences or whatever, but I don't know it. 06:09:06 well 06:09:19 suppose first that f and g are paths 06:09:30 so f, g : [0, 1] \to X 06:09:36 are continuous 06:09:47 a homotopy is now a "rectangle" between them 06:10:09 is this rectangle actually an infinite dimensional hypercube 06:10:14 nope 06:10:16 i think it's just a rectangle 06:10:18 it's just a rectangle 06:10:23 wow, that's a relief. 06:10:36 it's h : [0, 1] \times [0, 1] \to X such that h(x, 0) = f(x) and h(x, 0) = g(x) for all x \in X 06:10:41 erm 06:10:45 it's h : [0, 1] \times [0, 1] \to X such that h(x, 0) = f(x) and h(x, 1) = g(x) for all x \in X 06:11:01 ARGH 06:11:04 one last try. 06:11:14 it's h : [0, 1] \times [0, 1] \to X such that h(x, 0) = f(x) and h(x, 1) = g(x) for all x \in [0, 1] 06:11:22 ^ that should be right. 06:11:22 well i got the point regardless. 06:11:39 i only used the fact that they are paths so that i could call it a rectangle 06:11:43 that's the general definition 06:11:54 so one [0,1] is how far you are along the path and the other is how far you are between paths. 06:12:01 exactly 06:12:03 is it related to natural transformations somehow 06:12:59 maybe there's a whatever between functors and paths. 06:13:09 now as such this is kind of trivial: if the space X is path-connected, any two functions are homotopic 06:14:01 paths defined like this can't actually be composed in an associative way, right 06:14:11 but you can for example choose x \in [0, 1] and y \in X (in the case of paths above) and restrict to functions such that f(x) = y 06:14:25 shachaf: well X doesn't have to be the unit interval... 06:14:38 (and the homotopies must also go through only such functions, so that h(x, t) = y for all time parameters t) 06:14:40 so that kind of... puts a damper on things 06:14:55 i really shouldn't've called the codomain X 06:15:08 oh, you meant that about functors being them. well sucks to be a path 06:15:22 shachaf: they can if you consider them only up to homotopy equivalence 06:15:45 clearly one should compose paths by having f(1) = g(0) and just stringing them along 06:16:11 since non-associativity only comes from the fact that (f \circ f') \circ f'' and f \circ (f' \circ f'') are parametrized differently 06:16:31 Bike: you can, but that's only associative up to homoropy equivalence. 06:16:37 and also homotopy 06:17:00 i think Bike means that you can end up with a path : [0, 2] -> X or something 06:17:02 i really appreciate that you're taking the time to explain this to someone who's only half awake 06:17:05 oh 06:17:13 but yes that's what i meant, though shrinking the interval 06:17:21 shrinking? 06:17:21 yeah you shrink 06:17:32 shachaf: just making it [0,1] instead of [0,2]. 06:17:39 if you do that then you don't get associativity anymore 06:17:48 without this homotopy equivalence thing oklofok is talking about 06:17:58 so paths f and g compose into h(x) = f(2x) if x < 0.5 and h(x) = g(...) otherwise 06:18:06 where ... is something really complicated 06:18:24 like maybe (x-0.5)*2 06:18:34 sounds hard 06:18:40 yeah i looked it up 06:19:00 you can also compose homotopies, the exact same way 06:19:11 (you shrink time) 06:19:11 shachaf means if you did that then you'd get different shrinkages for (f.g).h and f.(g.h) though. 06:19:22 yes, and that's what i initially addressed 06:19:24 well, probably. if he doesn't then pretend i did. 06:19:27 yes, hence the whole "only up to homotopy equivalence" 06:19:28 not this trivial issue 06:19:36 aw man 06:19:46 but if you did allow arbitrary [0,n] intervals then you'd get associativity 06:20:04 but then you have f : [0,1] -> X and g : [0,2] -> X which ought to be the same but aren't and who wants that 06:20:08 yeah but you wouldn't get for example an identity path 06:20:24 yeah 06:20:24 you'd get an identity path for each n 06:21:36 usually you want that the space forms a category with each point an object and each path a morphism, and that they form a category. for this you need shrinkage. 06:21:43 because otherwise you don't have an identity 06:22:04 right 06:22:12 Bike: so where does this endofunctor business come in 06:22:30 why in god's name are you listening to me 06:22:38 you are the resident category theory expert 06:22:45 you heard oklofok 06:22:59 you're the category person around here 06:23:41 never category i didn't liek 06:24:24 i'm going to chile in a few weeks to talk to people about category theory 06:24:52 are you visiting california while you're at it 06:24:57 good place to visit imo 06:25:13 this article is available in the (closed) library but not online. do i live in a fucking cave 06:25:35 no but i'll visit jfk! 06:25:39 for 10 hours! 06:25:42 Bike: at least you have a library :'( 06:25:45 good ten hours 06:25:52 shachaf: pretty much the best thing about school 06:25:54 cool, gcmap will tell you the farthest airport from any airport 06:26:05 oklofok: i've done that 06:26:12 the whole "10 hours at jfk" thing 06:26:28 it'll be my first visit to us 06:26:30 it's an "ok airport to wait in i guess" 06:26:35 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...). 06:26:40 are you just flying through or actually visiting 06:26:54 after i stopped smoking, airports are pretty boring 06:27:02 just flying through 06:27:20 kmc: SLC had indoor smoking rooms "how weird is that" 06:27:28 odd 06:27:29 what's slc 06:27:47 Salt Lake City International Airport 06:27:53 don't all airports have those 06:28:23 -!- quintopia has quit (*.net *.split). 06:28:36 I don't know. 06:28:40 unless it's so small you can just go outside 06:29:00 so what's the usual topology on R anyway 06:29:17 the order topology which is also the topology given by the obvious metric 06:29:25 i don't know anything about metrics 06:29:34 well 06:29:38 absolute value of difference 06:29:42 gives the metric 06:29:44 and err 06:30:01 if you have a metric, then you get a topology by taking the radius r balls around each point as a basis 06:30:28 where balls just means open intervals i suppose 06:30:31