search

UniMath / agda-unimath

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

Equivalences of synthetic categories #1181

Closed ivankobe closed 2 weeks ago

ivankobe commented 2 weeks ago

Defined sections, retractions and equivalences of synthetic categories and proved lemma 1.1.6. from the book.

EgbertRijke commented 2 weeks ago

Awesome!

We have some pre-commit functionality, which must be run using make pre-commit from the terminal.

pre-commit is a python package that can be installed separately, see the agda-unimath installation guide if you don't have it yet.