## Stream: math-comp users

### Topic: Two versions of the same data structure

#### Ricardo (Feb 22 2023 at 15:39):

Hi everyone. Hope you're all well. I have a data structure for graph homomorphisms like

``````Record hom (S N : choiceType) : Type :=
Hom { dom : graph S N
; cod : graph S N
; f_sites : {fmap S -> S}
; f_nodes : {fmap N -> N}
; property1 : ...
}.
``````

Then all the homomorphims that share the codomain are the objects of a comma category. That's why I'd like to parameterise some homomorphisms over their codomain like

``````Record cHom (S N : choiceType) (cod : graph S N) : Type :=
CHom { dom : graph S N
; f_sites : {fmap S -> S}
; f_nodes : {fmap N -> N}
; property1 : ...
}.
``````

so that I can write functions like

``````Definition cmatch S N (C : graph S N) (a b : cHom S N C) := ...
``````

I could also write `cHom` like

``````Record cHom (S N : choiceType) (C : graph S N) : Type :=
CHom { h :> hom S N
; codEcod : cod h = C
}.
``````

But I'm not sure what would be the advantages or disadvantages of each approach. What do you think would be a good way to share the theory for `hom` and `cHom`?

#### Paolo Giarrusso (Feb 22 2023 at 17:18):

Can you define hom in terms of cHom rather than the opposite?

#### Paolo Giarrusso (Feb 22 2023 at 17:19):

very roughly sth like

``````Record Hom S N := {
dom : graph S N
cod : graph S N
graph : cHom S N dom cod
}.
``````

#### Paolo Giarrusso (Feb 22 2023 at 17:20):

the upside is that instead of `codEcod`, you just never introduce two codomains that must be equal — which is the best way to replace propositional equalities by definitional ones

#### Paolo Giarrusso (Feb 22 2023 at 17:21):

I did this for both `cod` and `dom` not because it's necessary but because it seems more natural, might come up later, and this is of course somewhat invasive on the existing theory

#### Ricardo (Feb 22 2023 at 17:36):

Paolo Giarrusso said:

the upside is that instead of `codEcod`, you just never introduce two codomains that must be equal — which is the best way to replace propositional equalities by definitional ones

Yes, that's why I stopped. I knew that propositional equality would be a pain later on and there had to be a better way. Thank you @Paolo Giarrusso for the suggestion.

#### Ricardo (Feb 23 2023 at 02:08):

Your idea @Paolo Giarrusso of having both `dom` and `cod` as parameters has been increadibly useful. Together with having finfuns instead of finmaps for `f_sites` and `f_nodes` have made the proofs much shorter and clearer. Thank you.

#### Paolo Giarrusso (Feb 23 2023 at 02:18):

I haven't done so much but I'm happy it helped! For some context: "Bundling" and "unbundling" components are relatively common and general refactorings: bundling turns indexes/parameters into record members, and unbundling does the opposite. I've learned the idea from https://arxiv.org/abs/1102.1323 (even if their application to overloading, or algebraic hierarchies like math-comp, has significant performance problems at scale)

#### Ricardo (Feb 23 2023 at 03:11):

Yes. I read their paper when I started this project and even though their proposal seemed very compelling, their performance issues and the fact that I didn't find much documentation nor supporting libraries for that type of programming made me backtrack and search for other alternatives. Another paper I found interesting was the one by @Jason Gross https://arxiv.org/abs/1401.7694 but using HoTT scared me because I don't understand it yet.

#### Ali Caglayan (Feb 26 2023 at 19:15):

You may be interested in https://github.com/jwiegley/category-theory which uses similar ideas to Jason's library (such as uni polymorphism and avoidance of prop etc). That is compatible with regular Coq developments.

#### Ali Caglayan (Feb 26 2023 at 19:16):

The use of HoTT in Jason's library isn't particularly important for most things, but it does let you derive extensionality principles like isos ~ equalities. In practice however, this does not matter much in my experience.

#### Ricardo (Feb 26 2023 at 22:47):

Thank you @Ali Caglayan. Question: why would one want to avoid prop? Question 2: Uni polymorphism is universe polymorphism?

#### Ali Caglayan (Feb 26 2023 at 22:53):

HoTT has it's own reasons for avoiding prop (incompabibility with univalence) but the main reason it is avoided here is that it generalizes nicely. You could develop a whole theory about prop valued relations, but then you need to repeat a lot for homs (since they might be type valued). Then it is typically better to do type valued stuff from the begining. Same for Coq Ensembles vs presheaves.

See the reasons for the category-theory library here: https://github.com/jwiegley/category-theory/#design-decisions

#### Ricardo (Feb 27 2023 at 02:28):

I see. Thank you :smile:

Last updated: Jul 25 2024 at 15:02 UTC