Skip to content
📵
This account has been ∞-suspended. (Topologically.)
📵
This account has been ∞-suspended. (Topologically.)
Pro
Block or report user

Report or block favonia

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse

Organizations

@clf @g0v
Block or report user

Report or block favonia

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse

Pinned

  1. Forked from guillaumebrunerie/initiality

    A formalized proof of a version of the initiality conjecture

    Agda

  2. Development of homotopy type theory in Agda

    Agda 320 55

  3. The People's Refinement Logic

    Standard ML 205 18

  4. "Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

    OCaml 155 12

142 contributions in the last year

Jun Jul Aug Sep Oct Nov Dec Jan Feb Mar Apr May Mon Wed Fri
Activity overview
Contributed to RedPRL/cooltt, favonia/hdtt2020-notes, favonia/yuujinchou and 5 other repositories
Loading

Contribution activity

May 2020

Created a pull request in RedPRL/cooltt that received 13 comments

Refactor cof checking

This is an experiment for fun.

+220 −158 13 comments

Created an issue in RedPRL/cooltt that received 5 comments

REPL command deliminator

What should be the delimiter between top-level commands, if any? normalize 5; normalize 5;;

5 comments

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

You can’t perform that action at this time.