That's great -- thank you very much, Paul.

@PaulTaylor Well, Bauer and Lumsdaine are saying that Bourbaki-Witt is not constructive in the sense that it holds in all toposes, so I'm still confused by your remark. Could I trouble you for the title of Wilson's paper? I may ask Andrej or Peter to comment.

@PaulTaylor Then I think I want to know what people mean by "constructive", because Bauer and Lumsdaine claim it cannot be proven intuitionistically (and I believe them), here: arxiv.org/abs/1201.0340. Can you shed some light on this?

If they are to be related to ring theory, then the crucial axiom to consider is the distributive law: $a \wedge (b \vee c) = (a \wedge b) \vee (a \wedge c)$ [where it is helpful to think of $\wedge$ as 'multiplication' and $\vee$ as 'addition']. Unlike ring theory, though, it follows from this distributive law and the other lattice axioms that also 'addition' distributes over 'multiplication'. You can get some distance with such analogies, but they shouldn't be pushed too far.

@PeterLeFanuLumsdaine Oh, I see. Very nice! And simple indeed. Thank you!

@RobertFurber Thank you.

@MartinSleziak Thank you!

Neither page exists any more.

@MartinSleziak Yes, that was the one. Maybe some day I'll get back to it (although I think the nLab has disabled some of the personal pages).