| 15 Jul 2020 |
 @swaraj-:matrix.org | same | 15:08:51 |
 seanmoss | This afternoon I tried to get back into it by trying to prove some elementary number theory in Cubical Agda. It's been interesting to see how difficult basic things are since, for example, equality isn't defined inductively any more. | 15:09:43 |
| @swaraj-:matrix.org | ok let's say break this week and the next | 15:09:48 |
| @swaraj-:matrix.org | so we reconvene on the 29th | 15:09:57 |
| @swaraj-:matrix.org | in the meanwhile people could list things they'd like to discuss or something | 15:10:10 |
| seanmoss | Some people have expressed interest in actually doing some maths - possibly non-higher dimensional - happy to work co-operatively on this if people want | 15:11:05 |
| seanmoss | In reply to @swaraj-:matrix.org
so we reconvene on the 29th Sounds good | 15:11:13 |
| 29 Jul 2020 |
 Nick Hu | How do people feel about meeting today? Does anyone have anything that they'd especially like to talk about? | 10:01:11 |
| @swaraj-:matrix.org | maybe sean can talk about what he's been working on and we can discuss how we can join in? | 13:50:17 |
| @swaraj-:matrix.org | also one of us can set up a meeting room if you don't always want to host, nick | 13:50:50 |
| @swaraj-:matrix.org | just to make it easy for you | 13:51:04 |
| @swaraj-:matrix.org | nick maybe just host today's thing anyway since that's the default link everyone goes on | 13:58:20 |
| @swaraj-:matrix.org | and we can discuss what to do then | 13:58:24 |
| Nick Hu | Sure, I don't mind | 13:58:36 |
| @swaraj-:matrix.org | sweet | 13:58:41 |
| seanmoss | sorry, missed this | 15:01:35 |
| seanmoss | are we meeting? | 15:01:37 |
 Fabian Zaiser | I can't joint the Hangouts call | 15:06:24 |
| @swaraj-:matrix.org | sec | 15:06:32 |
| @swaraj-:matrix.org | maybe nick needs to let you in | 15:06:36 |
| @swaraj-:matrix.org | who is currently taking care of his cat who is vomitting | 15:06:49 |
| @swaraj-:matrix.org | so it might take a minute | 15:06:52 |
| Fabian Zaiser | Oh, ok | 15:07:02 |
| 30 Jul 2020 |
| Nick Hu | Summer Recess
Until the beginning of next term, let's postpone our regular weekly meetings and meet on-demand instead: anyone may call a meeting, to be held at the next provisional 4pm Wednesday slot, but otherwise we won't meet regularly. Of course, Discourse isn't going anywhere so feel free to post on that still!
| 12:31:31 |
| 21 Aug 2020 |
|  Jesper Cockx joined the room. | 12:21:27 |
| Jesper Cockx changed their display name from jcockx to Jesper Cockx. | 12:21:45 |
| Jesper Cockx | Hi! I wanted to try out how Matrix works and maybe create an Agda channel here but I saw there's this one already. So I hope you don't mind me bumping in. | 12:23:17 |
| Jesper Cockx | Now that I'm here I might as well ask you about your opinions on Matrix/Element vs other solutions such as Slack, Zulip, or Discourse. | 12:24:00 |
| Nick Hu | Hi Jesper! Nice to meet you | 12:24:19 |
| Nick Hu | The biggest issue with Matrix is when people (like us unfortunately) use the matrix.org homeserver, which is severely over capacity (https://t2bot.io/docs/2020-matrix-org-lag/). This causes events, e.g. push notifications and messages, to sometimes be severely delayed | 12:25:32 |
