Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A 2-categorical analysis of context comprehension

Greta Coraglia, Jacopo Emmenegger

TL;DR

By recognising terms as coalgebras, it is shown how to use the structure-semantics adjunction to prove that a 2-category of comprehension categories is biequivalent to a 2-category of (non-discrete) categories with families.

Abstract

We consider the equivalence between the two main categorical models for the type-theoretical operation of context comprehension, namely P. Dybjer's categories with families and B. Jacobs' comprehension categories, and generalise it to the non-discrete case. The classical equivalence can be summarised in the slogan: "terms as sections". By recognising "terms as coalgebras", we show how to use the structure-semantics adjunction to prove that a 2-category of comprehension categories is biequivalent to a 2-category of (non-discrete) categories with families. The biequivalence restricts to the classical one proved by Hofmann in the discrete case. It also provides a framework where to compare different morphisms of these structures that have appeared in the literature, varying on the degree of preservation of the relevant structure. We consider in particular morphisms defined by Claraimbault-Dybjer, Jacobs, Larrea, and Uemura.

A 2-categorical analysis of context comprehension

TL;DR

By recognising terms as coalgebras, it is shown how to use the structure-semantics adjunction to prove that a 2-category of comprehension categories is biequivalent to a 2-category of (non-discrete) categories with families.

Abstract

We consider the equivalence between the two main categorical models for the type-theoretical operation of context comprehension, namely P. Dybjer's categories with families and B. Jacobs' comprehension categories, and generalise it to the non-discrete case. The classical equivalence can be summarised in the slogan: "terms as sections". By recognising "terms as coalgebras", we show how to use the structure-semantics adjunction to prove that a 2-category of comprehension categories is biequivalent to a 2-category of (non-discrete) categories with families. The biequivalence restricts to the classical one proved by Hofmann in the discrete case. It also provides a framework where to compare different morphisms of these structures that have appeared in the literature, varying on the degree of preservation of the relevant structure. We consider in particular morphisms defined by Claraimbault-Dybjer, Jacobs, Larrea, and Uemura.
Paper Structure (18 sections, 18 theorems, 34 equations, 1 figure)

This paper contains 18 sections, 18 theorems, 34 equations, 1 figure.

Table of Contents

  1. Introduction
  2. A biadjunction between comonads and adjunctions
  3. Morphisms of adjunctions and of comonads
  4. The 2-reflection between comonads and adjunctions
  5. The right adjoint $\mathrm{EM}$
  6. The 2-reflector $\mathrm{C}$
  7. The counit
  8. The unit
  9. The trianguar identities
  10. The bireflection for loose morphisms
  11. The 2-categories of interest
  12. The 2-category of comprehension categories
  13. Weakening and contraction comonads
  14. The 2-category of generalised categories with families
  15. The biequivalence between comprehension categories and generalised categories with families
  16. ...and 3 more sections

Key Result

Theorem 2.7

There is a 2-reflection \begin{tikzcd}[column sep=6em] \cmdCat \ar[r,shift right=1ex,hook,"\cmdtoadj"{swap}] \ar[r,phantom,shift left=.3ex,"\adj{-90}"{description}] & \adjLCat \ar[l,shift right=1.5ex,"\adjtocmd"{swap}] \end{tikzcd}such that the counit is the identity $\mathrm{C} \circ \mathrm{EM} =

Figures (1)

  • Figure 1: The underlying diagrams in $\mathbf{Cat}$ of, from left to right, a comprehension category, a w-comonad, and a generalised category with families.

Theorems & Definitions (64)

  • Definition 2.1
  • Remark 2.2
  • Definition 2.3
  • Remark 2.4
  • Remark 2.5
  • Definition 2.6
  • Theorem 2.7
  • Lemma 2.8
  • proof
  • Corollary 2.9
  • ...and 54 more