Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: event: MIT Categories Seminar

Topic: March 26 - David Myers' talk

Paolo Perrone (Mar 24 2020 at 18:51):

Hello all. This is the official topic of discussion for David Myers' talk, "Homotopy Type Theory for doing Category Theory".
Date and time: Thursday, March 26, 12 noon EDT (Boston time).
Streaming link here: https://youtu.be/1xm8vDwWf3Y .

Brendan Fong (Mar 24 2020 at 21:02):

Yay, looking forward to this -- been wanting to understand this better for some time

Joe Moeller (Mar 24 2020 at 21:15):

Wow great. This should be cool.

Paolo Perrone (Mar 26 2020 at 15:54):

Dear all,

Apparently YouTube has a nationwide problem with live streaming today, so we cannot have the seminar there.
We will use Zoom instead. Please all come to this call:

Join Zoom Meeting
https://zoom.us/j/667324456?pwd=akVmZlM4T01uZjlpZzl1VEpSRW1Vdz09
Meeting ID: 667 324 456
Password: 562708

Sorry for the inconvenience and for the short notice.

See you there!
Paolo

Matteo Capucci (he/him) (Mar 26 2020 at 15:57):

Do we still use this chat or Zoom's?

Brendan Fong (Mar 26 2020 at 15:58):

We'll use here in Zulip

Brendan Fong (Mar 26 2020 at 15:59):

(It has better threading, and is easier to browse for people who can't join us live)

Paolo Perrone (Mar 26 2020 at 15:59):

Welcome everyone! We are about to start. We are on Zoom!

Matteo Capucci (he/him) (Mar 26 2020 at 16:02):

Brendan Fong said:

We'll use here in Zulip

:thumbs_up:

Georgios Bakirtzis (Mar 26 2020 at 16:03):

Does anybody else have problems with sound?

Alex Rice (Mar 26 2020 at 16:03):

It is very stuttery for me

Mike Stay (Mar 26 2020 at 16:04):

ditto

Matteo Capucci (he/him) (Mar 26 2020 at 16:05):

Same

Paolo Perrone (Mar 26 2020 at 16:05):

I hear it well. Sorry to hear you are not!
In any case, we are recording locally, so that in case of connection problems (of the speaker or of the audience), there will be an HD video up to re-watch!

Alex Rice (Mar 26 2020 at 16:05):

I can still hear ok enough

Alex Kavvos (Mar 26 2020 at 16:10):

st-t-t-t-t-ttuter!

Emily Riehl (Mar 26 2020 at 16:12):

It seems I missed the memo (for not being on the mailing list). Can someone share the zoom link?

Matteo Capucci (he/him) (Mar 26 2020 at 16:12):

Some messages above

Mike Stay (Mar 26 2020 at 16:12):

https://zoom.us/j/667324456?pwd=akVmZlM4T01uZjlpZzl1VEpSRW1Vdz09

Emily Riehl (Mar 26 2020 at 16:13):

Thanks

Mike Stay (Mar 26 2020 at 16:15):

Does the expression $\prod_{a:A} B(a)$ assume that A has elements?

Alex Rice (Mar 26 2020 at 16:15):

don't think so

Mike Stay (Mar 26 2020 at 16:16):

How about "pairs (a,b) s.t. a:A, b:B"? That looks awfully set-like.

Thomas Read (Mar 26 2020 at 16:18):

What do you mean by "has elements"?

Alex Kavvos (Mar 26 2020 at 16:18):

Mike Stay said:

Does the expression $\prod_{a:A} B(a)$ assume that A has elements?

you should think of its elements like functions $f : A \to \cup_{a \in A} B_a$, such that $f(a) \in B_a$. so if $A$ is empty, it will also be empty.

Matteo Capucci (he/him) (Mar 26 2020 at 16:20):

(deleted)

Mike Stay (Mar 26 2020 at 16:21):

While we're paused: can he move his mouse pointer off the middle of the slide?

Matteo Capucci (he/him) (Mar 26 2020 at 16:24):

I answered my question myself

Emily Riehl (Mar 26 2020 at 16:27):

@Mike Stay The use of "(a,b) : A x B" is just notation. You could equally state the rule as

(formation rule) Given types A and B there is a type A x B.
(introduction rule) Given a : A and b : B there is a term p : A x B.
(elimination rule) Given any x : A x B there are terms y : A and z : B.
(computation rule) If you apply the elimination rule to a term formed by the introduction rule you get a : A and b : B back.
(other computation rule) If you apply the introduction rule after the elimination rule you get x : A x B back.

Mike Stay (Mar 26 2020 at 16:32):

The stutter seems to be a volume-related issue. When he starts to talk quietly, zoom stops transmitting clearly.

Philipp G. Haselwarter (Mar 26 2020 at 16:41):

Nothing wrong with talking about the elements of a type. The term term just evokes syntax, and the intuition that type theory is about syntax has to die. In the same vein, set theory will soon disappear, and element will naturally be used to describe the things that inhabit types ;)

Gershom (Mar 26 2020 at 16:56):

i tend to disagree. the "element" relation makes one think of working with some form of set. "inhabitant" is a better word imho.

Nathanael Arkor (Mar 26 2020 at 16:58):

that type theory is about syntax has to die

I very much disagree :)

Nathanael Arkor (Mar 26 2020 at 16:58):

concrete syntax and grammars, yes, but not abstract syntax

Paolo Perrone (Mar 26 2020 at 17:06):

Thanks everyone for coming! Late questions are always welcome, here in this thread :)
We will upload the video to Youtube as soon as possible.

Pierre Cagne (Mar 26 2020 at 21:03):

Couldn't attend. Will there be a video uploaded on the Youtube channel in spite of the streaming not having happened on Youtube?

Mike Stay (Mar 26 2020 at 21:16):

Yes, they recorded the talk using Zoom and will upload it eventually.

Paolo Perrone (Mar 26 2020 at 22:19):

Hi all! Here is the video of today's talk. https://youtu.be/nalC40POVLU
We did our best to improve the quality combining the two recordings. Some "stuttering" is still there, but the talk should be understandable. Sorry again for the technical glitches, we really didn't expect that YouTube could go down!

James Fairbanks (Mar 27 2020 at 18:05):

@Paolo Perrone what software do you use for recording the video of the person superimposed on the video of the slides?

Paolo Perrone (Mar 27 2020 at 18:11):

@James Fairbanks OBS, and I have to say it works like a charm. https://obsproject.com/