Commutative idempotent binary operations with eventually idempotent right action imply sethood

[fredrik-bakke]

Gives a generalisation of David Wärn's result that the algebraic structure of a semilattice implies sethood.

Theorem. Given a type $A$ with a binary operation ${-}*{-}$ that satisfies

1. idempotence ($x * x = x$)
2. commutativity ($x * y = y * x$)
3. eventual idempotence of the right action, meaning that for each $y$ there is a natural number $n$ such that, letting $r(x) := x * y$, then $r^{n+1}(x) = r^n(x)$ for all $x$

then $A$ is a set.

[fredrik-bakke]

I'll mark this PR as ready for review once I've found the time to re-review the comments I received on my CSB-WLPO pull request, to avoid having you repeat feedback you've given me before.

[fredrik-bakke]

Actually, shortly after posting this I realised I have a couple more generalisations of these facts.

EDIT: Nevermind, I've just stared at this for too long and started imagining things.

[tomdjong]

I'm going to unsubscribe from this PR until it's ready for PR (just to avoid a lot of emails about commits). Please ping me when it's ready. Thanks!

[martinescardo]

Gives a generalisation of David Wärn's result that the algebraic structure of a semilattice implies sethood.

Theorem. Given a type A with a binary operation − ∗ − that satisfies

1. idempotence (
     x
     ∗
     x
     =
     x
   )

2. commutativity (
     x
     ∗
     y
     =
     y
     ∗
     x
   )

3. eventual idempotence of the right action, meaning that for each 
     y
    there is a natural number 
     n
    such that, letting 
     r
     (
     x
     )
     :=
     x
     ∗
     y
   , then 
     
       r
       
         n
         +
         1
       
     
     (
     x
     )
     =
     
       r
       n
     
     (
     x
     )
    for all 
     x

then A is a set.

Is this motivated by something you have in mind?

[martinescardo]

Better name: if-every-loop-is-refl-then-the-type-is-a-set.

[fredrik-bakke]

Sorry, does that mean I should rename refl-is-set too?

[fredrik-bakke]

Is this motivated by something you have in mind?

The motivation was to see how far I could stretch the original result. I have some new results today though, so better conditions will/might follow soon.