Inconsistency between Iso and Category.isIso

[maxsnew]

The paths in Iso are called rightInv and leftInv while paths in isIso for Category are called sec and ret. I guess the most sensible refactor would be to change the name of the fields in isIso to match Iso since more code uses Iso.

[anshwad10]

personally I find sec and ret to be better names, so I'd rather rename the fields of Iso (though I realize that isn't as feasible, a lot of code uses isIso as well so it's gonna be a breaking change either way)

[mortberg]

I can never remember which is section and which is retraction, so right/leftInv feels a bit more intuitive to me

[maxsnew]

The main point in favor of calling them sec and ret is that the types of the field are called section ... and retract ... so there is some slight cognitive overhead of remembering that rightInv has type section ...

But I don't have strong feelings either way. I have had to adapt to both in working with the library.

[anshwad10]

another point in favor of sec and ret is that they have the same length as fun and inv which makes code look better aesthetically imo

[msyds]

Funny, I can never remember which is left and which is right }:P.

I would like to make a PR for this. Would it be overly ambitious / difficult to review if I were to go for (left|right)Inv → (ret|sec) despite the fact that more code uses Iso?

[msyds]

Just one more point for sec/ret over leftInv/rightInv: "left" and "right" are defined by whatever arbitrarily-chosen notation is used (i.e. function application in Iso and diagrammatic-order composition in isIso). If we renamed isIso's fields to leftInv/rightInv, they'd be swapped from Iso's leftInv/rightInv, which I'd argue is an even worse inconsistency. "Section" and "retraction" have a clear meaning regardless of how you write composition/application.

[maxsnew]

I agree that retract and section are better names because right/left relies on an arbitrary notational choice as you say.

But there is still ambiguity: does the field sec say that fun is a section or that inv is a section? I was kind of surprised that the fields are saying inv is a section/retraction of fun. I'm not suggesting that we change it, and there is already a "nota bene" comment on retract to this effect. But I would probably add to that comment that the way to read section f g is "g is a section of f". A completely unambiguous naming IMO would be to rename section to an infix g isSectionOf f.

[msyds]

A completely unambiguous naming IMO would be to rename section to an infix g isSectionOf f.

That would be most ideal, yes. }:) ❤️