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.

@article{paperbot1348,
  title = {2-adjoint equivalences in homotopy type theory},
  author = {Daniel Carranza and Jonathan Chang and Chris Kapulkin and Ryan Sandford},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 1},
  year = {2021},
  doi = {10.23638/lmcs-17(1:3)2021}
}