Port PLFA to work with agda-2.7 and stdlib-2.1

[JacquesCarette]

Summary of routine changes:

• use .Base for many modules instead of the "fat" top-level modules
• don't use any deprecated modules under Function (Function.Equivalence, etc) and replace with Function.Bundles
• get ¬_ from Relation.Unary.Negation
• get all the decidable predicates from Relation.Nullary.Decidable where they now live
• partial clean up of useless imports

Must-be-done changes that may need a bit more text:

• _≡⟨⟩_ is now syntax, so need to import step-≡-∣ instead
• step-≡ is now step-≡-⟩
• data List′ : Set → Set where is no longer equivalent to List (and doesn't even typecheck anymore with an option to allow large eliminations). I replaced the codomain with Set₁ and added a short sentence about it. I would actually recommend deleting List' entirely as the "better" change.

Stylistic changes to fit the 2.1 style better:

• in a couple of places, use contradiction instead of ⊥-elim

[JacquesCarette]

Predictably, the build failed. My skills at CI may not be up to changing the scripts to fix that. Help?

[wadler]

Thanks very much for doing this, Jacques!

I will ask Wen to look at fixing the CI. She is submitting her PhD dissertation just now, so it may take a while.

Following are suggested changes to your pull request. Can you modify to include these?

Induction, line 31, should be:
(Importing step-≡-I defines _≡⟨⟩_ and importing step-≡-⟩ defines _≡⟨_⟩_.)

Lists, lines 68-69, should be:
This is almost equivalent, save that with parameterised types the result can be Set,
whereas for technical reasons indexed types require the result type to be Set₁.

[JacquesCarette]

Will do a little later today.

[wadler]

Thanks! I've written to Wen to ask when she can update the CI. When does your term begin? (Edinburgh begins week 3 of September.)

[wadler]

Oops, I see Induction, line 24, also needs to change:
Old: cong, sym, and _≡⟨_⟩_, which are explained below:
New: cong, sym, _≡⟨⟩_ and _≡⟨_⟩_, which are explained below:

[wadler]

Also, a couple of background questions:

Was your intention to change ⊥-elim to contradiction everywhere it appears? I think I spotted some places where ⊥-elim was left unchanged.

Where can I read up on the change that leads to most imports ending .Base?

[wenkokke]

@JacquesCarette did you update the git submodule for the standard library? There's a bunch of Agda errors on CI that make me believe it's still using the older version.

[JacquesCarette]

When does your term begin?

Next Tuesday, September 3rd.

Was your intention to change ⊥-elim to contradiction everywhere it appears?

Probably not everywhere: it makes sense in part 1 to define it as it is. But, in practice, contradiction tends to make it clearer to the reader what is going on. I can certainly be more systematic if that is desired.

Where can I read up on the change that leads to most imports ending .Base?

There is, as of yet, no single place. There is a lot of conversation in stdlib issues and PRs related to that.

The design of the library (since 2.0) is to put the most basic definitions for X in Data.X.Base, the properties of X in Data.X.Properties and then have a "batteries included" module Data.X. So Data.X tends to be a convenient import when just getting work done, and then one tends to clean up afterwards for more precision and faster loading speed.

[JacquesCarette]

@wenkokke I neither updated the git submodule for the standard library nor the version of Agda in this PR. Obviously, I did do that in my working environment, but not through a git submodule for stdlib but rather through Agda's own library management features.

My git & CI powers are currently insufficient to be confident in making those changes correctly.

[wenkokke]

Also, a couple of background questions:

Where can I read up on the change that leads to most imports ending .Base?

Presumably, the changelog for agda stdlib.

This is likely a continuation of the trend towards more lightweight modules, so it's not essential, but probably shaves some time off the checking.

[wenkokke]

@wenkokke I neither updated the git submodule for the standard library nor the version of Agda in this PR. Obviously, I did do that in my working environment, but not through a git submodule for stdlib but rather through Agda's own library management features.

My git & CI powers are currently insufficient to be confident in making those changes correctly.

I'll add an entry to CONTRIBUTING.md while I do it.

[wenkokke]

Closing this in favour of #1028.

(@JacquesCarette you disallowed maintainers pushing to your branch, so I've made my own copy of your branch.)

[JacquesCarette]

That was a mistake - I wanted the exact opposite, i.e. allow maintainers to push! I could fix it... I would want the 'credit' of doing official, accepted PRs on here.

[JacquesCarette]

I've now allowed edits. Sorry about that.