| --- Log opened Tue Feb 07 00:00:36 2017 |
| 00:21 | | Kindamoody is now known as Kindamoody[zZz] |
| 00:31 | | Derakon[AFK] is now known as Derakon |
| 02:34 | | ion_ [Owner@Nightstar-6grqph.vs.shawcable.net] has quit [Ping timeout: 121 seconds] |
| 04:16 | | LadyOfLight` [catalyst@Nightstar-nu9noq.dab.02.net] has joined #code |
| 04:18 | | LadyOfLight [catalyst@Nightstar-d6v9pf.dab.02.net] has quit [Ping timeout: 121 seconds] |
| 04:20 | | gnolam_ [lenin@Nightstar-t1tbf0.cust.bahnhof.se] has joined #code |
| 04:23 | | gnolam [lenin@Nightstar-t1tbf0.cust.bahnhof.se] has quit [Ping timeout: 121 seconds] |
| 05:16 | | Derakon is now known as Derakon[AFK] |
| 05:42 | | himi [sjjf@Nightstar-dm0.2ni.203.150.IP] has quit [Ping timeout: 121 seconds] |
| 06:21 | | celticminstrel is now known as sleepyminstrel |
| 07:21 | | LadyOfLight` is now known as LadyOfLight |
| 07:23 | | LadyOfLight` [catalyst@Nightstar-kl6nuj.dab.02.net] has joined #code |
| 07:25 | | LadyOfLight [catalyst@Nightstar-nu9noq.dab.02.net] has quit [Ping timeout: 121 seconds] |
| 07:34 | | [R] [rstamer@genoce.org] has quit [Ping timeout: 121 seconds] |
| 07:34 | | [R] [rstamer@Nightstar-d7h8ki.org] has joined #code |
| 07:34 | | mode/#code [+ao [R] [R]] by ChanServ |
| 08:15 | | LadyOfLight` [catalyst@Nightstar-kl6nuj.dab.02.net] has quit [Ping timeout: 121 seconds] |
| 08:16 | | [R] [rstamer@genoce.org] has quit [Ping timeout: 121 seconds] |
| 08:16 | | [R] [rstamer@Nightstar-d7h8ki.org] has joined #code |
| 08:17 | | mode/#code [+ao [R] [R]] by ChanServ |
| 08:23 | | himi [sjjf@Nightstar-v37cpe.internode.on.net] has joined #code |
| 08:23 | | mode/#code [+o himi] by ChanServ |
| 08:41 | | LadyOfLight [catalyst@Nightstar-kl6nuj.dab.02.net] has joined #code |
| 08:44 | | Alek [Alek@Nightstar-cltq0r.il.comcast.net] has quit [Ping timeout: 121 seconds] |
| 08:48 | | Alek [Alek@Nightstar-cltq0r.il.comcast.net] has joined #code |
| 08:48 | | mode/#code [+o Alek] by ChanServ |
| 08:57 | | Vornicus [Vorn@ServerAdministrator.Nightstar.Net] has quit [Ping timeout: 121 seconds] |
| 09:43 | | LadyOfLight [catalyst@Nightstar-kl6nuj.dab.02.net] has quit [The TLS connection was non-properly terminated.] |
| 09:43 | | LadyOfLight [catalyst@Nightstar-kl6nuj.dab.02.net] has joined #code |
| 10:02 | | Kindamoody[zZz] is now known as Kindamoody |
| 10:50 | | mac [macdjord@Nightstar-5b2l0q.mc.videotron.ca] has joined #code |
| 10:50 | | mode/#code [+o mac] by ChanServ |
| 10:53 | | macdjord [macdjord@Nightstar-5b2l0q.mc.videotron.ca] has quit [Ping timeout: 121 seconds] |
| 11:19 | | gnolam_ is now known as gnolam |
| 11:19 | | mode/#code [+o gnolam] by ChanServ |
| 13:50 | | sleepyminstrel is now known as celticminstrel |
| 13:53 | | LadyOfLight` [catalyst@Nightstar-46h1ki.dab.02.net] has joined #code |
| 13:56 | | LadyOfLight [catalyst@Nightstar-kl6nuj.dab.02.net] has quit [Ping timeout: 121 seconds] |
| 14:18 | | LadyOfLight` is now known as LadyOfLight |
| 14:57 | | Derakon[AFK] [Derakon@Nightstar-5mvs4e.ca.comcast.net] has quit [Ping timeout: 121 seconds] |
| 15:40 | | mac is now known as macdjord|wurk |
| 16:03 | <@sshine> | why is it when you're at a party and someone asks what type theory really is, and you point to the mathematicians in the crowd and say that they can probably better explain it, they say "What's Type Theory?" |
| 16:03 | < LadyOfLight> | :p |
| 16:03 | < LadyOfLight> | Because it's category theory? x) |
| 16:05 | <@sshine> | I thought type theory was this foundation of mathematics that computer scientists just happen to really like because it lets you reject non-constructive axioms. but I'm not sure why that should be so unpopular among mathematicians that they've never heard of it... |
| 16:06 | <@sshine> | *is* it category theory? I've never really understood the connection except that they both seem like ways to explain a lot of mathematics at once. :) |
| 16:06 | <@sshine> | I'm not even sure a lot of categories are well-defined in variants of (homotopy) type theory. |
| 16:07 | <@sshine> | (I think homotopy type theory is a variant of type theory that's more popular among computer scientists.) |
| 16:13 | < LadyOfLight> | I'm really not even slightly an expert |
| 16:28 | | Vornicus [Vorn@ServerAdministrator.Nightstar.Net] has joined #code |
| 16:28 | | mode/#code [+qo Vornicus Vornicus] by ChanServ |
| 16:55 | | Kindamoody is now known as Kindamoody|afk |
| 18:02 | | Reiv [NSwebIRC@Nightstar-ih0uis.global-gateway.net.nz] has quit [Ping timeout: 121 seconds] |
| 18:35 | | Kindamoody|afk is now known as Kindamoody |
| 20:16 | | Derakon [Derakon@Nightstar-5mvs4e.ca.comcast.net] has joined #code |
| 20:16 | | mode/#code [+ao Derakon Derakon] by ChanServ |
| 20:23 | | LadyOfLight` [catalyst@Nightstar-7he.jtr.132.82.IP] has joined #code |
| 20:25 | | LadyOfLight [catalyst@Nightstar-46h1ki.dab.02.net] has quit [Ping timeout: 121 seconds] |
| 21:05 | | Kindamoody [Kindamoody@Nightstar-0lgkcs.tbcn.telia.com] has quit [Connection reset by peer] |
| 21:06 | | Kindamoody|autojoin [Kindamoody@Nightstar-0lgkcs.tbcn.telia.com] has joined #code |
| 21:06 | | mode/#code [+o Kindamoody|autojoin] by ChanServ |
| 21:07 | | Kindamoody|autojoin is now known as Kindamoody |
| 21:14 | | himi [sjjf@Nightstar-v37cpe.internode.on.net] has quit [Ping timeout: 121 seconds] |
| 21:30 | | LadyOfLight [catalyst@Nightstar-bt5k4h.81.in-addr.arpa] has joined #code |
| 21:34 | | LadyOfLight` [catalyst@Nightstar-7he.jtr.132.82.IP] has quit [Ping timeout: 121 seconds] |
| 21:43 | | Reiv [NSwebIRC@Nightstar-ih0uis.global-gateway.net.nz] has joined #code |
| 21:43 | | mode/#code [+o Reiv] by ChanServ |
| 22:03 | | Kindamoody is now known as Kindamoody|afk |
| 22:58 | <&[R]> | <nulluser> "Are you rectally-sourcing your information?" |
| 23:05 | | himi [sjjf@Nightstar-dm0.2ni.203.150.IP] has joined #code |
| 23:05 | | mode/#code [+o himi] by ChanServ |
| 23:29 | | Kindamoody|afk is now known as Kindamoody |
| --- Log closed Wed Feb 08 00:00:37 2017 |