Popular repositories Loading

1. PhD-thesis PhD-thesis Public

   My PhD thesis.

   TeX 13

2. Setoid-Universe Setoid-Universe Public

   Rocq Prover 5

3. cwf-strictification cwf-strictification Public

   Accompanying formalisation for the paper "Type theory in type theory using a strictified syntax"

   HTML 3

4. observational-coq observational-coq Public

   Forked from Yann-Leray/coq

   Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

   OCaml 2

5. strict-setoids strict-setoids Public

   A strict setoid model based on PMP's strict presheves

   Agda 1

6. cubical cubical Public

   Forked from agda/cubical

   Agda