TL;DR
This paper introduces the concept of 2-adjoint equivalences within Homotopy Type Theory, establishing their properties and formalizing the results in the Lean Theorem Prover.
Contribution
It defines and explores 2-adjoint equivalences in Homotopy Type Theory, providing formal proofs using the Lean Theorem Prover.
Findings
Defined (half) 2-adjoint equivalences in HoTT
Proved their expected properties
Formalized results in Lean
Abstract
We introduce the notion of (half) 2-adjoint equivalences in Homotopy Type Theory and prove their expected properties. We formalized these results in the Lean Theorem Prover.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
