It was pointed out to me in a private communication that the tuple function \x->(x,x) is actually a special case of a diagonalization for biapplicative and some related structures monadicially. Another example in the same flavor is pure impl for the applicative instance for sized lists. diag x = bipure x x So framed a litttle differently, there’s definitely an abstraction or common pattern lurking here. Perhaps folks can help Tease this out. One person I chatted with this morning alluded to it being relevant to computational flavors of adjunctions or some such ? It def matters in a different way when doing computation resource aware programming in a symmetric monoidal category. Let’s collect some ideas and patterns and get to the bottom of this!