A followup on the Top view #1923

[jamesmckinna]

NOW: rebased to make direct use of #1923's Top view.

[jamesmckinna]

Hmmm, that all went swimmingly, save for the seeming re-addition/committal of Data.Fin.Relation.Unary.Top after the rebase... will attempt to cherry-pick my way out of there. But failing that, I could always rebase jamesmckinna:top-view and try to merge from there.

Anyway: now the definitions don't use Instances, but do streamline away all the pointless not-equal-to reasoning that went before in the definition and properties of lower₁... so please consider as candidate refactoring... ;-)

[gallais]

will attempt to cherry-pick my way out of there

No need to bother. If the diff is correct then it's fine: we'll squash the PR when merging anyways!

[gallais]

Looks good!

[jamesmckinna]

So the only outstanding question(s) would be:

• which of lower₁ or inject₁⁻¹ belongs in README.Data.Fin.Relation.Unary.Top, or both (basically exporting them over from Lower, and removing that module; or leaving lower₁ in Lower, and inject₁⁻¹ in Top etc.)?
• do we refactor Data.Fin.Properties now to use the Top view directly? (probably: not this time?)
• can we do similar to Data.Fin.Base (this would I think involve in-lining the view in that module, so maybe not?) to be able to define opposite and lower₁ directly...?

[jamesmckinna]

Last few commits are perhaps a little... eccentric. Suggest I/we sit on this one for a while... it was me trying to advance an agenda of 'refactor Data.Fin.Base/Properties to simplify certain definitions and proofs', as well as propagandising about views... so a period of reflection is (probably) in order ;-)

[jamesmckinna]

I haven't managed to return to this for the last six months, and I think I don't see myself being able to in the immediate future, so closing for the time being. I may return to it at a later date, but I suspect it's milestone:v3.0, if ever.