mechvel

> Is this #153? Not precisely. #153 suggests a single module Data that exports "everything of Data" -- which looks strange to me, something like joining all the standard library...

Suppose that you join all the standard Data export, and that you need ``+-comm`` for Integer. Will ``Data.+-comm`` be for ``Integer._+_``, for ``Nat._+_``, or for ``Bin._+_`` ? In my suggestion,...

JacquesCarette: > what @mechvel is after is what Bill Farmer and I called high level theories. > [..] Not necessary "high level" . I meant _some "theory" related to the...

Not precisely. I mean 1) Change the first letter in the record name to the lower case. 2) Append the character ᶜ Example: ``` record IsGCD ... where constructor isGCDᶜ...

It is desirable to have a final decision announced.

> I don't quite know what you mean by "it looks like an ordinary function name, as not necessarily a record > constructor.". Seeing ``(fooᶜ x y ...)`` the reader...

Currently I define and use ``` RELRespects : REL A B ℓ → Rel A ℓ₁ → Rel B ℓ₂ → Set _ RELRespects _~_ _~₁_ _∼₂_ = ∀ {x...

I do not see these lemmas in Algebra.Properties.Magma.Divisibility in lib-2.0. Do you mean that they have to appear in the next official version?

I see there that ``_∤_`` is imported, but I do not see there the three suggested proofs ``` ∤-resp : _∤_ Respects₂ _≈_ ... ``` For any occasion: the last...

These lines concern ``_∣_`` - divisibility. And I talk about ``_∤_`` - negation of divisibility. Are you saying that ``∣-respʳ`` is also a proof for ``_∤_ Respectsʳ _≈_`` ? (I...