> you will immediately see that it is not the case that {{a,1},{b,2}} = {{a},{a,b}}. This is true for the examples you gave i.e. Agda and Coq but this is not a

> you will immediately see that it is not the case that {{a,1},{b,2}} = {{a},{a,b}}. This is true for the examples you gave i.e. Agda and Coq but this is not a theoretical restriction. As long as you can formalize equality with something like axiom of univalence, you can prove similar things (e.g. forall x, f(x) = g(x) => f=g which gives interesting applications like mergeSort = quickSort). Proving univalence constructively is pretty hard, but it's at least partially solved, e.g. cubic type theory can constructively prove univalence. Agda has a branch that has cubic type theory implemented, if you want to check it out. There is also an "official" implementation of cubic type theory by the team who wrote the original paper but it's a pretty lean programming language without even unification.