Jon Sterling

I think we don't support deep patching, as in `S # [foo.bar := baz]`; nonetheless, this is a useful and important feature of ML-style module systems that could be nice...

Consider returning to strict universes

6

I had decided to use cooltt to experiment with weak universes, i.e. universes where the decoding laws hold up to iso. These are fine, but they make certain things harder...

We should have something like ```ocaml type 'a pattern val match_tp : D.tp -> 'a pattern -> 'a m ``` An example would be something like: ```ocaml let* base, fam...

It doesn't look very good right now 😆

Proposal to extend boundary-sensitive refinement to positive types

2

Right now the boundary sensitive refinement via extension types only works for negative types. In particular we can reduce `(M,N) : A * B [phi -> U]` to `M :...

I noticed a bug in the handling of pushing a substitution under a BindSym. Who else can see it? 🤦🏻‍♂️🤣 (Btw only saw this using 🧠, didn’t find an error...

Add "refinement" type connective

1

I have discovered a much more implementable version of Orton-Pitts strictification/realignment. 1. Take a `phi`-modal type, i.e. `A : {phi} type` 2. Take family of `phi`-connected types indexed in `A`,...

An idea for abstract function interfaces

2

Functions out of inductive types are defined by eliminators, but this has unfortunate effects: if we unfold the function, then we get the whole brutal eliminator expression, and it is...

Let the user define an Open Modality

1

I had a nice idea for a cool use of the cofibration machinery. If the user can declare a fresh cofibration, then this is basically enough to define a strict...