For example, let’s take very simple structure.

Structure smth A := {

op: A -> A -> A;

op_comm: forall x y, op x y = op y x

}.

How to make/model “subsmth”? Or maybe work around somehow?

For example, let’s take very simple structure.

Structure smth A := {

op: A -> A -> A;

op_comm: forall x y, op x y = op y x

}.

How to make/model “subsmth”? Or maybe work around somehow?

This is what I got. Let’s hope I didn’t mess anything up in such short code.

```
Structure smth A := {
op: A -> A -> A;
_: forall x y, op x y = op y x
}.
Definition injective A B (f: A -> B) := forall x y, f x = f y -> x = y.
Definition subsmth A B (sA: smth A) (sB: smth B): Prop :=
exists (f: A -> B), injective f /\ forall x y, f (op sA x y) = op sB (f x) (f y).
```

1 Like