Steven Schaefer

Soliciting nicknames for Finn

So far I’ve got:
Finasteride
FinSet
Finn the human

Ooooo the lichess app now has a modern ui on iOS

What a day to be alive

🐻‍❄️ Animal #835 🦆
I figured it out in 2 guesses!
🟧🟩
🔥 1 | Avg. Guesses: 12.6

https://metazooa.com
#metazooa

@amy @ncf @totbwf

After looking at the gist I have a couple questions:

1. You write "types living in Typeω do not yet support the Kan operations transp and hcomp", and the last time I checked there was a similar message in the Agda documentation. I'm very curious what "yet" means in this context. The gist makes it sound infeasible at the moment, but the following paragraphs suggest there is reason to believe that these operations will eventually be worked out. Do you have thoughts in the direction of an implementation, or perhaps good pointers if one wished to take a stab at it? I've long wished to have a large path type, as it would allow for a nice implementation of large category theory. However, I don't have much experience with the Agda internals, so I do not know where to begin

2. Re "Rewrite rules are actually pretty useful!": The title of this section led me to believe that Mikan would encourage usage of rewrite rules, but the content of the section seems to suggest that rewrite rules must be dropped to preserve safety. Is this correct? Meaning that the correct interpretation of the second paragraph in this section is that in the absence of --rewriting, one can safely emulate their interface by using J on path constructors of a HIT?

I have been working almost exclusively in the --cubical fragment of Agda, so I'm excited to see where this project goes! Best of luck!

wow if i multitask, my language skills go to 0. (rapidly editing all the typos in my latest toots)