Kazuhiko Sakaguchi

BTW, why CI disappeared from the checklist here?

> @spacekitteh Where was https://coq.inria.fr/refman/Reference-Manual031.html#sec776 pointing to? https://coq.inria.fr/distrib/V8.15.0/refman/addendum/parallel-proof-processing.html?highlight=parallel#proof-annotations

@spitters We did not consider adding a structure of join semilattices because the canonical `meetSemilatticeType` instance of `T^d` should work as the canonical join semilattice of `T` where `^d` stands...

The first issue is that the class record of `latticeType` should include two semilattice mixins to implement proper inheritance from join semilattices to lattices, but now actually it does not....

Thinking about definitionally involutive duals, I also believe that `[latticeType of (A *p B)^d]` and `[latticeType of A^d *p B^d]` should be convertible.

`dual (dual T) = T` holds for some particular instances, but in general, it does not. ```coq Goal forall d (T : pt d), dual (dual T) = T. reflexivity....

I have attempted to implement a complete duality of structures without having some dual structures, but my conclusion is that it seems impossible. For example, we have `porderType`, `bPorderType`, and...

I have added join-semilattice structures and some order structures with a top but without a bottom anyway. I hope this will be helpful to implement the order structures and definitionally...

Documentation is not done yet and finmap has to be fixed. Except that, this PR is ready for review. But we have an option not to merge this PR and...

@CohenCyril Would you like to review and merge this PR soon? I'm not requesting to include this in 1.12. But I would like to know whether it is reasonable to...