Now that I've touched the `functions.v`

file a bit, I'm starting to understand things better. This is definitely a dramatic improvement over the existing approach. I did have a handful of questions here

- Applying theorems with HB based arguments was not what I was expecting. Several times I got opaque error messages. If I have a theorem

```
Lemma example (f : {bij A >-> B}) : P f
```

and I have an `f : X -> Y`

in scope, and my goal is `P f`

. I'd like to write just `apply: example`

, and then have a remaining goal that says

```
f is a bijection
```

Unfortunately, I just get an error about how the tactic failed to apply. Is there an better way to do this? How would you even write the `f is a bijection`

thing as a goal? I would be fine to create a bespoke HB instance for `f`

in the middle of my proof. The difficulty is determining exactly what instance to create.

- I've been thinking about extending this with mixins for continuity and homeomorphisms. Is that where you were planning on going with this approach? It's infeasible to change everything at once, so is there an existing technique for incrementally changes?

Zachary Stone said:

Now that I've touched the

`functions.v`

file a bit, I'm starting to understand things better. This is definitely a dramatic improvement over the existing approach. I did have a handful of questions here

- Applying theorems with HB based arguments was not what I was expecting. Several times I got opaque error messages. If I have a theorem
`Lemma example (f : {bij A >-> B}) : P f`

and I have an

`f : X -> Y`

in scope, and my goal is`P f`

. I'd like to write just`apply: example`

, and then have a remaining goal that says`f is a bijection`

Unfortunately, I just get an error about how the tactic failed to apply. Is there an better way to do this? How would you even write the

`f is a bijection`

thing as a goal? I would be fine to create a bespoke HB instance for`f`

in the middle of my proof. The difficulty is determining exactly what instance to create.

- I've been thinking about extending this with mixins for continuity and homeomorphisms. Is that where you were planning on going with this approach? It's infeasible to change everything at once, so is there an existing technique for incrementally changes?

- Local instances are indeed problematic right now, the current solution is to use the
`Pbij`

helper lemma, as in`have /Pbij : set_bij A B f.`

. We have been and are going working on lighter solutions though. - Yes! The plan is to extend this with various kinds of morphisms (continuity, etc), and stuff. The main problem right now is that it will soon interfere with a parallel hierarchy (namely additive, rmorphism, etc) which is built by hand instead of HB. When https://github.com/math-comp/math-comp/pull/733 is finally merged, we might finally have the ability to merge both hierarchy.

2'. Also, a longer term goal of mine is to make HB generate structures and morphisms simultaneously (when appropriate) and provide the common language (symbols) and theory of category theory to handle them.

- Ah, that explains what those lemmas are doing. I figured I wasn't the first person to have the problem.
- Ah, generating the morphism is a nice touch. I'm all for the automation. But I'm no category theory expert. Is that an existing category theory library you'd leverage?

Last updated: Jan 30 2023 at 10:03 UTC