Speculative investigation of taking advantage of morita equivalence
To do so, we need to implement some category theoretic machinery.
It would be much better to port @JacquesCarette and @HuStmpHrrr 's agda categories library, but we probably want to introduce more eta-equality into the type-theory to gain all the dualisation benefits.
Speculative investigation of taking advantage of morita equivalence
To do so, we need to implement some category theoretic machinery.
It would be much better to port @JacquesCarette and @HuStmpHrrr 's agda categories library, but we probably want to introduce more eta-equality into the type-theory to gain all the dualisation benefits.