2 Search Results for "Kudasov, Nikolai"

Document

DOI: 10.4230/LIPIcs.ITP.2025.20

Formalizing Colimits in 𝒞at

Authors: Mario Carneiro and Emily Riehl

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract

Certain results involving "higher structures" are not currently accessible to computer formalization because the prerequisite ∞-category theory has not been formalized. To support future work on formalizing ∞-category theory in Lean’s mathematics library, we formalize some fundamental constructions involving the 1-category of categories. Specifically, we construct the left adjoint to the nerve embedding of categories into simplicial sets, defining the homotopy category functor. We prove further that this adjunction is reflective, which allows us to conclude that 𝒞at has colimits. To our knowledge this is the first formalized proof that the nerve functor is a fully faithful right adjoint and that the category of categories is cocomplete.

Cite as

Mario Carneiro and Emily Riehl. Formalizing Colimits in 𝒞at. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{carneiro_et_al:LIPIcs.ITP.2025.20,
  author =	{Carneiro, Mario and Riehl, Emily},
  title =	{{Formalizing Colimits in 𝒞at}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.20},
  URN =		{urn:nbn:de:0030-drops-246186},
  doi =		{10.4230/LIPIcs.ITP.2025.20},
  annote =	{Keywords: category theory, infinity-category theory, nerve, simplicial set, colimit}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2023.10

E-Unification for Second-Order Abstract Syntax

Authors: Nikolai Kudasov

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract

Higher-order unification (HOU) concerns unification of (extensions of) λ-calculus and can be seen as an instance of equational unification (E-unification) modulo βη-equivalence of λ-terms. We study equational unification of terms in languages with arbitrary variable binding constructions modulo arbitrary second-order equational theories. Abstract syntax with general variable binding and parametrised metavariables allows us to work with arbitrary binders without committing to λ-calculus or use inconvenient and error-prone term encodings, leading to a more flexible framework. In this paper, we introduce E-unification for second-order abstract syntax and describe a unification procedure for such problems, merging ideas from both full HOU and general E-unification. We prove that the procedure is sound and complete.

Cite as

Nikolai Kudasov. E-Unification for Second-Order Abstract Syntax. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 10:1-10:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kudasov:LIPIcs.FSCD.2023.10,
  author =	{Kudasov, Nikolai},
  title =	{{E-Unification for Second-Order Abstract Syntax}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{10:1--10:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.10},
  URN =		{urn:nbn:de:0030-drops-179944},
  doi =		{10.4230/LIPIcs.FSCD.2023.10},
  annote =	{Keywords: E-unification, higher-order unification, second-order abstract syntax}
}

Refine by Type
2 Document/PDF
1 Document/HTML

Refine by Publication Year
1 2025
1 2023

Refine by Author
1 Carneiro, Mario
1 Kudasov, Nikolai
1 Riehl, Emily

Refine by Series/Journal
2 LIPIcs

Refine by Classification
1 Theory of computation → Equational logic and rewriting
1 Theory of computation → Logic and verification

Refine by Keyword
1 E-unification
1 category theory
1 colimit
1 higher-order unification
1 infinity-category theory
Show More...

2 Search Results for "Kudasov, Nikolai"

Formalizing Colimits in 𝒞at

Abstract

Cite as

E-Unification for Second-Order Abstract Syntax

Abstract

Cite as

Thanks for your feedback!

Could not send message