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

Idea

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

Definition

A tabular dagger 2-poset is a dagger 2-poset $C$ such that for every object $A:Ob(C)$ and $B:Ob(C)$ and morphism $R:Hom(A,B)$, there is an object $\vert R \vert:Ob(C)$ and maps $f:Hom(\vert R \vert, A)$, $g:Hom(\vert R \vert, B)$, such that $R = f^\dagger \circ g$ and for every object $E:Ob(C)$ and maps $h:Hom(E,\vert R \vert)$ and $k:Hom(E,\vert R \vert)$, $f \circ h = f \circ k$ and $g \circ h = g \circ k$ imply $h = 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.