Block or report user



Popular repositories

  1. Chromiarch-OS

    A way to run both Chrome OS and Arch Linux simultaneously on a Samsung Chromebook

    Shell 11 2

  2. reversetreeenhancer

    User script for a better experince when using a reverse tree on Duolingo

    JavaScript 11 3

  3. HoTT

    Forked from HoTT/HoTT

    This repository is now obsolete

    Coq 9

  4. HoTT-Agda

    Forked from HoTT/HoTT-Agda

    Development of homotopy type theory in Agda

    Shell 3

  5. JamesConstruction

    Formalization of the James construction in Agda

    Agda 3

  6. agda

    Forked from masondesu/agda

    Agda is a dependently typed programming language / interactive theorem prover.


54 contributions in the last year

Oct Nov Dec Jan Feb Mar Apr May Jun Jul Aug Sep Mon Wed Fri

Contribution activity First pull request First issue First repository Joined GitHub

July - September 2017

guillaumebrunerie has no activity yet for this period.

June 2017

Created an issue in mortberg/cubicaltt that received 8 comments

Useless(?) hComp’s with empty systems when using higher inductive types

In the code below, the normal form of the term p is <!0> hComp SuspS1 (merid {SuspS1} (hComp S1 base []) @ !0) []. It seems strange that we get hCo…

Seeing something unexpected? Take a look at the GitHub profile guide.