Brendan Zabarauskas on Twitter: "@Blaisorblade Yeah, this is a super interesting project!" / Twitter

#TypeTheory: why does unbundling seem to never come up when discussing #Agda typeclasses? It seems to me the problem would apply in Agda as well as in Coq eelis.net/research/math-. Tagging

@jjcarett2

because he must have informed opinions on this...

Paolo G. Giarrusso

@Blaisorblade

Apr 17, 2020

Uh alhassy.github.io/next-700-modul seems relevant.

Brendan Zabarauskas

@brendanzab

Replying to

@Blaisorblade

Yeah, this is a super interesting project!

1:21 PM · Apr 17, 2020Twitter Web App

Conversation