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

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

# Contents

## Idea

A dagger 2-poset with elements with a good notion of relation comprehension of morphisms and elements.

## Definition

A relational dagger 2-poset $C$ is a dagger 2-poset with elements such that for objects $A:Ob(C)$ and $B:Ob(C)$ and for morphism $R:Hom(A,B)$ and elements $a:El(A)$ and $b:El(B)$, there is a type $R(a,b)$ with a term $p:isProp(R(a,b))$, and an identity

$q:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{D:Ob(C)} \prod_{R:Hom(A,B)} \prod_{S:Hom(B,C)} \prod_{a:El(A)} \prod_{d:El(D)} (S \circ R)(a, d) = \left[\sum_{b:El(B)} S(b,d) \times R(a,b)\right]$