[Agda] [ANNOUNCE] Agda Standard Library 1.4 release candidate 1

[mechvel at scico.botik.ru]

On 2020-08-31 16:32, Matthew Daggitt wrote:
> Dear all,
> 
> The Agda Team is pleased to announce the first release candidate of
> version 1.4 of the standard library.
> [..]

It is written there in CHANGELOG.md
"
  The module `Relation.Binary.PropositionalEquality` has been growing in 
size and
  now depends on a lot of other parts of the library, even though its 
basic
  functionality does not. To fix this some of its parts have been 
factored out.
   `Relation.Binary.PropositionalEquality.Core` already existed. Added 
are:
   ```agda
   Relation.Binary.PropositionalEquality.Properties
   Relation.Binary.PropositionalEquality.Algebra
   ```
These new modules are re-exported by 
`Relation.Binary.PropositionalEquality`
and so these changes should be invisble to current users, but can be 
useful
to authors of large libraries.
"

Can you, please, explain: what is the difference between writing
module Foo where
open import Relation.Binary.PropositionalEquality using (foo)
...
and
module Foo Where
open import Relation.Binary.PropositionalEquality.Core using (foo)
...
(assuming that foo is in ...Core)
?
Is the latter better for the authors of large libraries? Why?
Do you mean that fewer modules of standard library will be type-checked?
(because if PropositionalEquality is type-checked, then Agda needs to 
type-check
at list once all the modules it imports).
Does this make a difference to  Foo.agdai ?  its size?

Thanks,

------
Sergei