Is there a variant of canonical structures that can solve problems like TemplateMonad ?B = proj ?E x with ?B := x and ?E := <canonical structure with proj := TemplateMonad?

TemplateMonad ?B = proj ?E x

?B := x

?E := <canonical structure with proj := TemplateMonad

Last updated: Dec 07 2023 at 14:02 UTC