Homotopy Type Theory tabular dagger 2-poset > history (Rev #5)

Contents

Idea

A dagger 2-poset with tabulations, such as a tabular allegory.

Definition

A tabular dagger 2-poset is a dagger 2-poset CC such that for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) and morphism R:Hom(A,B)R:Hom(A,B), there is an object |R|:Ob(C)\vert R \vert:Ob(C) and maps f:Hom(|R|,A)f:Hom(\vert R \vert, A), g:Hom(|R|,A)g:Hom(\vert R \vert, A), such that R=f gR = f^\dagger \circ g and for every object E:Ob(C)E:Ob(C) and maps h:Hom(E,|R|)h:Hom(E,\vert R \vert) and k:Hom(E,|R|)k:Hom(E,\vert R \vert), fh=fkf \circ h = f \circ k and gh=gkg \circ h = g \circ k imply h=kh = k.

Properties

The category of maps of a tabular dagger 2-poset has all pullback?s.

Examples

The dagger 2-poset of sets and relations is a tabular dagger 2-poset.

See also

Revision on April 21, 2022 at 00:53:58 by Anonymous?. See the history of this page for a list of all contributions to it.