Commit 2024-08-06 09:11 c82a357f
View on Github →feat(ModelTheory/Substructures): define equivalences between substructures and prove simple results (#11175)
Define partial equivalences between structures. A partial equivalence between structures M and N is a subobject of M and a subobject of N along with an equivalence between. This is useful to build an actual equivalence between M and N.