Update to Agda 2.6.3

[WhatisRT]

Update ledger & the dependencies to Agda 2.6.3. This gives us a few nice things, in particular some improvements to metaprogramming and potentially quotients via erased cubical. It also means we don't have to rely on a custom patched version of Agda anymore.

[JaredCorduan]

🎉 🎊 🍾

[williamdemeo]

"...It also means we don't have to rely on a custom patched version of Agda anymore."

That is great news! 💯 👏🏼

...although, this branch doesn't type-check for me yet. I'll try to diagnose/fix it today.

[williamdemeo]

With @WhatisRT's mods to the emacs config instructions, this branch type-checks for me on macos darwin, intel chipset (xeon). Thank you @WhatisRT! 😄

[williamdemeo]

The changes are very minor---just pointing out that some imports are not used---so I'll approve the PR and leave it up to you whether or not to remove the unnecessary imports before merging.

[williamdemeo]

Should we not include the emacs config instructions on the main README as well as CONTRIBUTING? I think they're very useful and harder to find if they're only in CONTRIBUTING.

[williamdemeo]

It seems ¬? is not used. Can we delete this import?

I think we can also delete the following imports from src/Axiom/Set/Map.agda:

open import Axiom.Set.Factor th
import Data.List

[williamdemeo]

Same comment here. We could remove the following imports from src/Axiom/Set/Rel.agda:

open import Axiom.Set.Factor th
import Data.List
open import Relation.Nullary.Decidable using (¬?)

[williamdemeo]

In src/Axiom/Set/Sum.agda I think we can remove the following:

import Data.Sum
open Equivalence

[williamdemeo]

From src/Interface/Decidable/Instance.agda we can remove the following:

open import Data.List
open import Data.List.Properties
open import Relation.Nullary

As well as the variable P in the private variable declarations.

[williamdemeo]

From src/Ledger/PPUp/Properties.agda we could remove some imports.

open import Ledger.Epoch

open import Tactic.ReduceDec
open import MyDebugOptions

[williamdemeo]

More unused imports:

In src/Axiom/Set.agda: open import Relation.Nullary.Negation

In src/Axiom/Set/List.agda:

import Data.List.Relation.Unary.Any.Properties as Any
open import Relation.Nullary