Jon Sterling

This is done already by De Jong and Escardo in Agda: https://github.com/tomdjong/TypeTopology/blob/master/source/DcpoLimits.lagda. I'd like to have that in this library too.

Marcelo Fiore has been explaining his work on Abstract Domain Theory to me, and I think it would be nice to formalize some of it, especially over an arbitrary Grothendieck...

HierarchyBuilder causes a lot of noisy elpi-related warnings. I wonder if we can (or should) silence these...

https://github.com/coq/coq/releases/tag/V8.8.0

This clever operator I defined in order to validate the later modality rules without power objects being total can also be used to validate the intersection type rules, without using...

This would help make some examples more convincing.

When you reenter the app, it crashes if you try to reload the list of repositories.

Improve article 2202.07329

2

**Problem details** > Conversion to HTML had a Fatal error and exited abruptly. This document may be truncated or damaged. **Desktop (please complete the following information)** - OS: macOS -...