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

## Definition

A power dagger 2-poset is a dagger 2-poset $C$ such that for every object $A:Ob(C)$ there exists an object $\mathcal{P}(A)$ called the power object of $A$, a morphism $\in_A:Hom(A, \mathcal{P}(A))$ called subobject membership in $A$, such that for each morphism $R:Hom(A,B)$, there exists a morphism $\chi_R:(A,P(B))$ called the characteristic morphism such that $R = (\in_A^\dagger) \circ \chi_R$.

## Examples

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

## See also

Revision on April 20, 2022 at 01:29:11 by Anonymous?. See the history of this page for a list of all contributions to it.