Skip to content




  • Pro


@HoTT @Andromedans
Block or Report

Block or report andrejbauer

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse

Popular repositories

  1. plzoo Public

    Programming Languages Zoo

    OCaml 1.2k 67

  2. A course on homotopy theory and type theory, taught jointly with Jaka Smrekar

    TeX 244 8

  3. Spartan type theory

    OCaml 193 18

  4. marshall Public

    Real number computation software

    OCaml 106 13

  5. Homotopy Public archive

    Homotopy theory in Coq.

    Verilog 86 8

  6. coop Public

    A prototype programming language for programming with runners

    OCaml 77 2

326 contributions in the last year

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

Contribution activity

May 2022

Opened 5 pull requests in 2 repositories
andrejbauer/mathematics-and-computation 4 open
nikerzetic/lograc-project-2022-stop-logic 1 merged

Created an issue in kangrongji/cubical-classics that received 1 comment

These seem to be MacNeille reals.

Speaking intuitionistically, there are three kinds of reals, depening on how we phrase completeness: Cauchy reals: archimedean ordered field in wh…

1 comment

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