[[!redirects extensional dagger 2-posets]] #Contents# * table of contents {:toc} ## Idea ## A [[relational dagger 2-poset]] where morphisms satisfy the axiom of extensionality. ## Definition ## An extensional dagger 2-poset $C$ is a [[relational dagger 2-poset]] with a term $$p:\prod_{A:Ob(C)} \prod_{B:Ob(C)} \prod_{R:Hom(A,B)} \prod_{a:El(A)} \prod_{a^{'}:El(A)} \prod_{b:El(B)} \prod_{b^{'}:El(B)} (R(a,b) \times id_A(a,a^{'}) \times id_B(b,b^{'})) \to R(a^{'},b^{'})$$ ## See also ## * [[concrete dagger 2-poset]] * [[relational dagger 2-poset]] * [[Rel]]