Daniel Carranza ; Jonathan Chang ; Chris Kapulkin ; Ryan Sandford - 2-adjoint equivalences in homotopy type theory

lmcs:6778 - Logical Methods in Computer Science, January 22, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:3)2021
2-adjoint equivalences in homotopy type theory

Authors: Daniel Carranza ; Jonathan Chang ; Chris Kapulkin ; Ryan Sandford

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.


Volume: Volume 17, Issue 1
Published on: January 22, 2021
Submitted on: September 14, 2020
Keywords: Mathematics - Logic,Mathematics - Category Theory,03B38 Type theory (Primary), 18N10 2-categories, bicategories, double categories (Secondary)


Share

Consultation statistics

This page has been seen 164 times.
This article's PDF has been downloaded 114 times.