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

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

## Examples

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