Bjorn Ian Dundas
Bjorn Ian Dundas
P invisible squirrel A Bjorn On 1 Sept 2022, at 19:13, Daniel R. Grayson ***@***.***> wrote: 4. Tot P — Reply to this email directly, view it on GitHub,...
I agree that ”homotopy type” should have as small a place in the text as possible. A thing I liked about univalence is that it made my colloquialism ”up to...
Ouch, this was of course written long before 2.3 existed. Here’s my opinion. If we need to say much about the underlying universe before an informal remark as 4.2.21 is...
If we do such a thing, we should be careful of reminding the reader what type things have, especially if there have been a lot of equivalences along the way....