2-adjoint equivalences in homotopy type theory
Logic
2023-06-22 v4 Category Theory
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.
Keywords
Cite
@article{arxiv.2008.12433,
title = {2-adjoint equivalences in homotopy type theory},
author = {Daniel Carranza and Jonathan Chang and Chris Kapulkin and Ryan Sandford},
journal= {arXiv preprint arXiv:2008.12433},
year = {2023}
}