Anders Mörtberg

Remove two lines from .dir_locals

13

Could we please remove these lines from .dir_locals.el: ``` (modify-syntax-entry ?' "w") (modify-syntax-entry ?_ "w") ``` I very often want to erase an identifier to `_` but with these commands...

In Cubical Agda I can write things like: ``` sys : ∀ i → Partial (i ∨ ~ i) Set₁ sys i (i = i1) = Set → Set sys...

Add support for nested mutual blocks again

6

The PR https://github.com/mortberg/cubicaltt/pull/44 breaks support for nested mutual blocks.

Normalization/simplification function

2

I want a function similar to what we call "normal" in cubicaltt. The purpose of this function is to normalize/simplify terms as far as possible, this means that it has...

Self contained version of the new Brunerie number

1

This should probably not be merged, but I figured that it's easier to discuss it if we have a PR

I think it might be good to remove the Syntax folder and revert https://github.com/agda/cubical/pull/595 . The problem being that it causes problems when displaying goals

Move and clean stuff from AbGroup.Base

1

There's some stuff at the end of the file which should be somewhere else: https://github.com/agda/cubical/blob/master/Cubical/Algebra/AbGroup/Base.agda#L187 This should probably be done as part of a major overhaul of the Algebra files...

Move https://github.com/agda/cubical/tree/master/Cubical/Algebra/Group/EilenbergMacLane to Homotopy

I'm starting to think that we should: - Move compPath and friends to Foundations.Path - Move theory about transport to Foundations.Transport - Move lower HLevels to Foundations.HLevels Doing this will...

As discussed in https://github.com/agda/cubical/pull/264 it might make sense to use the SIP when developing CT. A first step would be to apply the cubical SIP to the various category structures...