Elektrine
EN
Log in Register
Paige Chat Timeline Communities Gallery Videos Email DNS VPN Uptime Kairo
Back to Timeline
Remote

VojtechStep

@VojtechStep@mathstodon.xyz
mastodon 4.6.4
  • Open on mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT.

I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

0 Followers
0 Following
10 Posts
Joined December 05, 2023
Website:
https://vojtechstep.eu/
GitHub:
https://github.com/VojtechStep

Posts

Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · May 12, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz

My doctoral school organizes an internal "doctorand day" where doctoral students from different domains are supposed to present their ideas to each other. As far as I know nobody really sees the value of this but participation is mandatory.

The program committee assigns every participant either a talk or a poster. A talk means you talk for 10 minutes and then you go home (/back to work). A poster means you need to be there the whole day.

Now, I got assigned a poster. I can't make them give me a talk, but I can try to make them regret giving me a poster (spite is a strong motivator for me, and I like to think I use it constructively).

So since I'm already recycling my topic from my TYPES talk, I decided to recycle the slides as well. Fortunately I had 8 of those, so perfect for just laying them out in a 2x4 grid. I now have both the slides and the poster importing the same slides-contents.typ file which defines all the text and revealing behavior. I'm only overriding polylux's alternatives-match function to work with handout mode, and everything else just works. I'm pretty happy with it!

4
0
0
0
Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · May 07, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz

The abstract and slides for our TYPES talk "Generating morphism types using parametricity and Trocq" are now available on my website, check them out! This is joint work with Cyril Cohen and Assia Mahboubi.

https://vojtechstep.eu/

10
0
5
0
Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · May 05, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz

LB:

4
0
0
0
Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · May 05, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz

UIP stands for Uomotopy Iype Pheory

3
1
0
0
Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · Apr 28, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz

@whitequark@social.treehouse.systems do the 88x31 buttons from grebedoc's website exist for git-pages?

0
2
0
0
Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · Apr 21, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz

Proof assistant called mikan

Implements cubicalTT instead of globularTT

This is what happens when you stray away from the path of the birb

0
0
0
0
Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · Apr 16, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz

Oh how I wish my server with the IRC bouncer hadn't died while I was in a different country

1
1
0
0
Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · Apr 16, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz

(the FSCD paper got rejected)

0
1
0
0
Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · Apr 16, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz

In an unexpected turn of events, this evening turned very disappointing (and I haven't even received any news on my FSCD submission). For context, this is what "no consensus" looks like:

Original proposed policy, closed: https://github.com/agda/agda/pull/8456
Current proposed policy:
https://github.com/agda/agda/pull/8507

4
0
1
0
Open post
VojtechStep
VojtechStep @VojtechStep@mathstodon.xyz · Mar 25, 2026
VojtechStep
@VojtechStep@mathstodon.xyz

PhD student on Inria's Gallinette team. Also working on synthetic homotopy theory in HoTT. I'm interested in (homotopy) type theory, formalization of mathematics, cats (the math kind) and cats (the fluffy kind).

mathstodon.xyz
5
0
1
0

Remote instance

mathstodon.xyz
Open on original server

Media

313k7r1n3
Elektrine

Tor hidden service

elekhj7afj4qnrr4yd3bkzslsyo5jgfxw3orgjkhlcxifueodybyiiad.onion

Platform

  • Email
  • Chat
  • Timeline
  • Communities
  • VPN
  • DNS

Company

  • About
  • Contact
  • FAQ

Legal

  • Terms of Service
  • Privacy Policy
  • Warrant Canary
  • Lite (no JS)
  • VPN Policy
  • Source code

Support

  • support@elektrine.com
  • Report Security Issue
Mail client setup IMAP mail.elektrine.com:993 POP3 mail.elektrine.com:995 SMTP mail.elektrine.com:465
© 2026 Elektrine. All rights reserved. Server: 05:40:36 UTC