This is a great talk, but the audio is defective. I hope you can find a opportunity to give this talk again with better audio, and add the video to this channel or your home page.
I was able to show that the precategory whose set of objects is 2=1+1 and with hom(a,b)=1 for all a,b in 2 is not a category. This is because, e.g. denoting the elements of 2 as x=inl(*) and y=inr(*), the identity type in 2 is (x=y) = 0 but the isomorphisms are (x≈y)=1. Now, how to see that if G is a group, then BG is not a category? If I can't get an answer here, can I have the link to the Zulip chat? Thank you all. Great talk.
around 39:00, the lemma is labeled UFP. What does UFP stand for, and what does it say about the lemma? Uniqueness of of Functoriality Proofs? Univalent Foundations Program? Univalent Fiber Principle? Uniqueness of Fibred Propositions?
I was curious as well. After listening a second time, then doing some online searching, I think "UFP" is the "[universal] fiber product" or 'pullback' where "[t]he pullback of two morphisms f and g need not exist, but if it does, it is essentially uniquely defined by the two morphisms." Sources: en.wikipedia.org/wiki/Pullback_(category_theory)#Fiber_bundles and en.wikipedia.org/wiki/Pullback_bundle
![โกหกเธอทั้งนั้น (Pinocchio) - SERIOUS BACON [Official MV]](http://i.ytimg.com/vi/P1HhTYwrR5A/mqdefault.jpg)
This is a great talk, but the audio is defective. I hope you can find a opportunity to give this talk again with better audio, and add the video to this channel or your home page.
I was able to show that the precategory whose set of objects is 2=1+1 and with hom(a,b)=1 for all a,b in 2 is not a category. This is because, e.g. denoting the elements of 2 as x=inl(*) and y=inr(*), the identity type in 2 is (x=y) = 0 but the isomorphisms are (x≈y)=1.
Now, how to see that if G is a group, then BG is not a category?
If I can't get an answer here, can I have the link to the Zulip chat?
Thank you all. Great talk.
around 39:00, the lemma is labeled UFP. What does UFP stand for, and what does it say about the lemma? Uniqueness of of Functoriality Proofs? Univalent Foundations Program? Univalent Fiber Principle? Uniqueness of Fibred Propositions?
I was curious as well. After listening a second time, then doing some online searching, I think "UFP" is the "[universal] fiber product" or 'pullback' where "[t]he pullback of two morphisms f and g need not exist, but if it does, it is essentially uniquely defined by the two morphisms."
Sources: en.wikipedia.org/wiki/Pullback_(category_theory)#Fiber_bundles and en.wikipedia.org/wiki/Pullback_bundle
granted the "[universal]" part might be "[unique]". it's hard to say.
There are a couple of theorems labeled 'UFP' and at least one labeled 'AKS'. They're references to the sources of the theorems given on the last slide