# Homotopy Type Theory tabular dagger 2-poset > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

## 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 exist is an object \vert R \vert \vert:Ob(C) called and atabulation of $R$ and maps $f:Hom(\vert R \vert, A)$ , and g:Hom(\vert R \vert, B) A) , such that R = g \circ f^\dagger \circ g , and for every object$E:Ob(C)$ and maps  h:Hom(E,A) h:Hom(E,\vert R \vert) and  k:Hom(E,B) k:Hom(E,\vert R \vert),  k f \circ h^\dagger h \leq = R f \circ k if and only if there exists a unique map j:E g \to \circ \vert h R = \vert g \circ k such imply that h = f k \circ j and $k = g \circ j$.

## 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.