Skip to content
View nimarasekh's full-sized avatar
😎
Always working!
😎
Always working!

Block or report nimarasekh

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.

Please don't include any personal information such as legal names or email addresses. Maximum 100 characters, markdown supported. This note will be visible to only you.
Report abuse

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

Report abuse
nimarasekh/README.md

Hi! Welcome to my GitHub Page

I am postdoc at the Universität Greifswald in Greifswald, Germany.

There I am a mathematician primarily interested in understanding the role of equalities in mathematics, otherwise known as homotopy theory.

I believe formalization of matheamtics via proof assistants can be an important step towards better understanding homotopy theory. As a result I have now commenced various formalization projects, including contributions to Coq UniMath and Rzk. In particular I am currently focused oon the following formalization projects:

  1. Double Categories: I am working on a formalization of double categories in Coq UniMath (jointly with Benedikt Ahrens, Paige North and Niels van der Weide).
  2. Formalization of ∞-Cosmoi: I have been contributing to the formalization of ∞-cosmoi due to Riehl and Verity via the proof assistant Lean.
  3. Simplicial Type Theory: I am contributing to the formalization of simplicial type theory, as defined by Riehl & Shulman.

More details my formalization work can be found in the repositories below!

More general information about me and my mathematical work can be found on my Academic Webpage.

Popular repositories Loading

  1. DVM DVM Public

    Forked from redavids/DVM

    ANU image analysis code "diamorse" -applied to materials science

    C++

  2. DoubleCategories DoubleCategories Public

    Formalization of Double Categories in UniMath via Coq

    Coq

  3. UniMath UniMath Public

    Forked from UniMath/UniMath

    This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

    Coq

  4. w3schools-test.github.io w3schools-test.github.io Public

    Forked from w3schools-test/w3schools-test.github.io

    w3schools.com repository used in demonstrating GitHub and GitHub pages

    HTML

  5. sHoTT sHoTT Public

    Forked from rzk-lang/sHoTT

    Formalisations for simplicial HoTT and synthetic ∞-categories.

    Markdown

  6. nimarasekh nimarasekh Public

    Repository for GitHub Page