search

gebner / hott3

HoTT in Lean 3
Apache License 2.0
75 stars 11 forks source link

Adjoint and two-adjoint equivalences #16

Closed daniel-carranza closed 4 years ago

daniel-carranza commented 4 years ago

This is a revision of the pull request we submitted (under Ryan Sandford) which proves additional results, removes redundant lemmas, and better integrates the built-in equivalence type.

From the previous pull request: "adj.lean contains definitions and theorems regarding half adjoint equivalences which formalize 4.2.3, 4.2.7, 4.2.9, 4.2.10, 4.2.12, and 4.2.13 from section 4.2 of the HoTT Book. 2adj.lean contains definitions and theorems regarding half 2-adjoint equivalences which formalize analogous theorems to that of 4.2.3, 4.2.12, 4.2.13 from section 4.2 of the HoTT Book."

daniel-carranza commented 4 years ago

Went ahead with all the suggestions listed here. I also removed the file hty_rec.lean and moved it into prelim.lean, since it only contained two results after clean-up.

fpvandoorn commented 4 years ago

Looks good. Thanks for the fixes!