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 theoryArticle

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.

    https://doi.org/10.23638/LMCS-17(1:3)2021
    Source: arXiv.org:2008.12433
    Volume: Volume 17, Issue 1
    Published on: January 22, 2021
    Accepted on: January 4, 2021
    Submitted on: September 14, 2020
    Keywords: Mathematics - Logic, Mathematics - Category Theory, 03B38 Type theory (Primary), 18N10 2-categories, bicategories, double categories (Secondary)
    Licence: Attribution 4.0 International (CC BY 4.0)
    Funding:
      Source : OpenAIRE Graph
    • Funder: Natural Sciences and Engineering Research Council of Canada

    Share and export

    Consultation statistics

    This page has been seen 2292 times.
    This article's PDF has been downloaded 843 times.