[[!redirects relational dagger 2-posets]] #Contents# * table of contents {:toc} ## 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]$$ ## See also ## * [[dagger 2-poset with elements]] * [[extensional dagger 2-poset]] * [[Rel]] * [[SEAR]] * [[Categorical SEAR]]