Bas Spitters

Congruence

9

For future reference. [This extension](http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_38) of the algorithm behind the congruence tactic that is compatible with HoTT.

Polygraphs in HoTT

6

By @MaximeLucasSky https://hal.archives-ouvertes.fr/hal-02385110 https://github.com/MaximeLucasSky/polygraphs

Rewrite

18

I am curious whether we can get this to work: Require Import HProp. Goal forall {A B:Type}, IsHProp A -> A B -> IsHProp B. intros ?? H e. rewrite

Switch to the new unification algorithm

6

@mattam82, @beta-ziliani have implemented a sane unification algorithm. https://github.com/unicoq/unicoq https://www.mpi-sws.org/~beta/unicoq.pdf We probably want to switch at some point when we are frustrated with incomprehensible unification errors.

Universe Comparator

3

This plugin allows to debug universe polymorphism. It may be useful. https://github.com/amintimany/UniverseComparator

smalltt

1

This is apparently very fast. Are any of the ideas useful in redtt? https://github.com/AndrasKovacs/smalltt

Strict Propositions

1

They will be available in Coq and agda, and if I understand things well they are consistent with CTT. Should we want them in redtt? https://github.com/coq/ceps/pull/37

The lemmas in this directory should be added to the stdlib and removed from corn. https://github.com/coq-community/corn/tree/master/stdlib_omissions

fiat cryptography

63

As requested at https://github.com/coq/platform/issues/28 opening an issue tracking: https://github.com/mit-plv/fiat-crypto/issues/925

SSProve

22

We'd like to add https://github.com/SSProve/ssprove to platform. Is there anything we'd need to do?