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

Showing changes from revision #2 to #3: 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 an object $\vert R \vert$ called a tabulation of $R$ and maps  p_A:Hom(\vert f:Hom(\vert R \vert, A) and  p_B:Hom(\vert g:Hom(\vert R \vert, B) such that  R = p_B g \circ p_A^\dagger f^\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.