pith. sign in

arxiv: 2401.11752 · v7 · pith:Y4MJW66Xnew · submitted 2024-01-22 · 💻 cs.LO · math.CT

Univalent Enriched Categories and the Enriched Rezk Completion

Niels van der Weide This is my paper

Pith reviewed 2026-05-24 04:36 UTC · model grok-4.3

classification 💻 cs.LO math.CT
keywords univalent enriched categoriesRezk completionenriched categorieshomotopy type theoryKleisli categoriesunivalent foundationscategorical equivalences
0
0 comments X

The pith

Univalent enriched categories make every essentially surjective fully faithful functor an equivalence and admit a Rezk completion.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that in univalent foundations, enriched categories that are univalent have the property that fully faithful and essentially surjective functors between them are equivalences. It also constructs a Rezk completion for any enriched category, which produces a univalent one. This completion is then applied to create univalent versions of enriched Kleisli categories. These results extend standard facts about ordinary categories to the enriched setting within homotopy type theory. A sympathetic reader would care because this provides a robust foundation for working with enriched structures in higher categorical and homotopical contexts.

Core claim

We prove that all essentially surjective and fully faithful functors between univalent enriched categories are equivalences, and we show that every enriched category admits a Rezk completion. Finally, we use the Rezk completion for enriched categories to construct univalent enriched Kleisli categories.

What carries the argument

The Rezk completion for enriched categories, which equips any enriched category with a univalent replacement while preserving the enrichment structure.

If this is right

  • Enriched categories can be replaced by univalent ones without losing information up to equivalence.
  • Univalent enriched Kleisli categories provide a setting for studying monads in enriched contexts with univalence.
  • Fully faithful and essentially surjective enriched functors can be used to detect equivalences in the univalent enriched setting.
  • Results from ordinary category theory about Rezk completions lift to the enriched case.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This framework could support more reliable semantics for programming languages that use enriched categories.
  • It opens the door to studying higher enriched categories with univalence.
  • Applications in homotopy theory might benefit from these completions for constructing univalent models.

Load-bearing premise

The proofs assume the ambient univalent foundations where equality is paths and that the enriching category satisfies univalence and completeness properties.

What would settle it

Finding an enriched category where no Rezk completion exists, or constructing a fully faithful essentially surjective functor between univalent enriched categories that is not an equivalence.

Figures

Figures reproduced from arXiv: 2401.11752 by Niels van der Weide.

Figure 1
Figure 1. Figure 1: Introduction rules for RH(C) 5.2. The Rezk Completion via HITs. Now we present another construction for Prob￾lem 5.1, but this time we use higher inductive types. Recall that higher inductive types are specified by a list of point constructors, path constructors, homotopy constructors, and so on. Given a category C, we are interested in the 1-truncated HIT RH(C) with a single point constructor rclC : C → R… view at source ↗
read the original abstract

Enriched categories are categories whose sets of morphisms are enriched with extra structure. Such categories play a prominent role in the study of higher categories, homotopy theory, and the semantics of programming languages. In this paper, we study univalent enriched categories. We prove that all essentially surjective and fully faithful functors between univalent enriched categories are equivalences, and we show that every enriched category admits a Rezk completion. Finally, we use the Rezk completion for enriched categories to construct univalent enriched Kleisli categories.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 1 minor

Summary. The paper develops the theory of univalent enriched categories in homotopy type theory. It proves that every essentially surjective and fully faithful functor between univalent enriched categories is an equivalence, shows that every enriched category admits a Rezk completion, and uses the Rezk completion to construct univalent enriched Kleisli categories.

Significance. If the results hold, this extends the univalent foundations program to enriched categories, providing a coherent treatment of enriched structures where equality of objects is given by paths. The work is significant for higher category theory, homotopy theory, and the semantics of programming languages, as it supplies the necessary univalent Rezk completions and equivalence characterizations without introducing free parameters or ad-hoc axioms. The construction of univalent Kleisli categories is a direct and useful application.

minor comments (1)
  1. The abstract and introduction should explicitly state the precise hypotheses on the enriching category (univalence and completeness) that are required for the Rezk completion to preserve the enrichment structure.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive evaluation of the manuscript and their recommendation to accept. We are pleased that the contributions to univalent enriched categories are viewed as significant for higher category theory and related areas.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper states and proves three main results in univalent foundations: essentially surjective fully faithful functors between univalent enriched categories are equivalences, every enriched category admits a Rezk completion, and the completion constructs univalent enriched Kleisli categories. These rest on the ambient homotopy type theory (paths as equalities) plus explicit hypotheses that the enrichment base is univalent and the completion preserves enrichment structure; none of the claims reduce by definition, by fitted parameters renamed as predictions, or by load-bearing self-citation chains to their own inputs. The derivation is therefore self-contained against external benchmarks in univalent category theory.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper operates inside univalent foundations; the central claims rest on the univalence axiom for the base of enrichment, the definition of enriched categories, and the standard properties of Rezk completion in ordinary categories. No free parameters or invented entities are visible from the abstract.

axioms (2)
  • domain assumption Univalence axiom: isomorphic objects are equal via paths
    Invoked implicitly by the use of 'univalent enriched categories' and the claim that fully faithful essentially surjective functors are equivalences.
  • standard math Existence of Rezk completion in the unenriched case
    Used as the base case that is lifted to the enriched setting.

pith-pipeline@v0.9.0 · 5601 in / 1439 out tokens · 23451 ms · 2026-05-24T04:36:02.342836+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.