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
.