Injective Objects and Fibered Codensity Liftings

TL;DR

This paper investigates fibered properties of functor liftings along fibrations, focusing on codensity liftings, and applies these findings to analyze bisimilarity-like notions in coalgebra theory.

Contribution

It identifies a sufficient condition for codensity liftings to be fibered, extending understanding of functor liftings in coalgebraic contexts.

Findings

A sufficient condition for codensity liftings to be fibered

Application of fibered liftings to bisimilarity-like notions

Extension of known results for Kantorovich lifting

Abstract

Functor lifting along a fibration is used for several different purposes in computer science. In the theory of coalgebras, it is used to define coinductive predicates, such as simulation preorder and bisimilarity. Codensity lifting is a scheme to obtain a functor lifting along a fibration. It generalizes a few previous lifting schemes including the Kantorovich lifting. In this paper, we seek a property of functor lifting called fiberedness. Hinted by a known result for Kantorovich lifting, we identify a sufficient condition for a codensity lifting to be fibered. We see that this condition applies to many examples that have been studied. As an application, we derive some results on bisimilarity-like notions.