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: Feb 06 2023 at 00:03 UTC