Trocq 0.1.7+prop

This is a demo release of Trocq, based on standard Coq/Rocq rather than HoTT.
Support for Prop has been added together with temporary axioms for proof irrelevance and prop extensionality.

Trocq 0.1.6

This is a demo version of Trocq.

Trocq 0.1.5

This is a demo version of Trocq.

Trocq 0.1.4

This is a demo version of Trocq.

Trocq 0.1.3

This is a demo version of Trocq.

Trocq 0.1.1

This is a demo version of Trocq.

Trocq 0.1.0

This is a demo version of Trocq, compatible with Coq 8.17 with Coq-HoTT and using a custom version of Coq-Elpi.

ESOP 2024

Artifact for the ESOP 2024 conference