Lifting Chain and TFAE to Sort

Stream: mathlib4

[Robert Maxton]

I have recently heard, to my mild dismay, that contributions (especially contributions from new contributors) to mathlib are suggested to keep to around 150 lines of code. As my ambivalent_def project has vastly exceeded that scale already, I'm going to start soliciting belated feedback on this project as I start dripping it into digestible pull requests.

[Robert Maxton]

The command (probably to end up being named tfai_def, for "(the following are isomorphic)-def") is meant to parallel the opaque command, but to follow up with a number of possible definitions; the idea being to handle in a semantically clear way definitions where no single canonical definition is to be preferred, and switching between definitions is to be possible at any time. As the new name implies, it is built on a lifting of List.TFAE into Sort, so that both the elements and the equivalences between them can be arbitrary Sorts. This in turn depends on a lifting of Chain into Sort; the two together have consumed most of my dev time. It's now mostly done, but it's a rather large set of files at this point.

[Robert Maxton]

In the first place, is this something Mathlib actually wants? (And doesn't already have, though I tried to check.)

[Yaël Dillies]

@Yury G. Kudryashov had thoughts about generalising tfae. I'm not sure what the status is

[Yury G. Kudryashov]

I thought about generalizing tfae to any partial order, not to Sort. What's the generalization of the "equality from a cycle of implications"?

[Robert Maxton]

I also was thinking about partial orders, but I realized that in my own planned use cases, I wanted to use data-carrying relations like FooEquiv

[Robert Maxton]

Partial orders are well and good but < is a relation that goes to Prop

[Robert Maxton]

So I ended up writing a TFAE l up to eqv notation and having a bunch of theorems that take a specific antisymm : r a b -> r b a -> eqv a b, or more generally a dependent antisymm : (f : r a b) -> (g : r b a) -> p f g -> eqv a b for some other predicate p