Skip to content
I reject my humanity
I reject my humanity




  • Pro
Block or Report

Block or report ice1000

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.

Add an optional note:
Report abuse

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

Report abuse

Hi there 👋 I go by Tesla Zhang. Typical usernames include ice1000 or tizusa.

  • 🌱 I have a blog, opensource-contributions, a resume, a research profile, an arXiv profile, and a codewars profile.
  • 🤔 I'm learning HoTT and is researching on its constructive interpretations, like cubical type theories.
    • I'm trying to implement CHM in Guest0x0.
    • I'm also interested in 2LTT and Andras Kovacs' ideas on staged programming with 2LTT.
    • I'm also XTT. Cool people are working on implementing it!
  • 👨‍💻 I'm currently working on a dependently-typed programming language Aya with some interesting ideas. It's going to be a practical proof assistant with programming features.
  • 💬 Ask me about IDEs, type theories and implementation of (univalent) dependent type systems!


  1. agda/agda Public

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

    Haskell 1.9k 258

  2. guest0x0 Public

    Neon lights in the night tonight and stars that shine in the open sky

    Java 32 2

  3. An experimental library for Cubical Agda

    Agda 321 108

  4. ~ Growing as cubes

    Java 141 4

  5. resume Public

    👾 My resume / 我的简历

    TeX 619 163

  6. jimgui Public

    💖 Pure Java binding for dear-imgui

    Java 151 14

Contribution activity

September 2022

Created a pull request in aya-prover/aya-dev that received 18 comments

Use cubical path in library

@imkiva help me with path eta

+357 −213 18 comments

Created an issue in aya-prover/aya-dev that received 28 comments

Pretty print precedence for interval expressions

Should have parenthesis

Opened 33 other issues in 5 repositories
aya-prover/aya-dev 10 open 11 closed
XmacsLabs/mogan 2 closed 7 open
sublimehq/Packages 1 open
sharkdp/bat 1 open
matchy233/chi-cv-template 1 open
21 contributions in private repositories Sep 8 – Sep 25

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