UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
222 stars 71 forks source link

Literature – Idempotents in Intensional Type Theory #1160

Closed fredrik-bakke closed 2 months ago

fredrik-bakke commented 3 months ago

Adds a literature file for the article Idempotents in Intensional Type Theory by Shulman. Most of sections 1-3, 5, and 9 are formalized.

1103 #1055

fredrik-bakke commented 2 months ago

merging time? 🥹👉👈

VojtechStep commented 2 months ago

👉😎👉