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

Showing changes from revision #4 to #5: Added | Removed | Changed

Contents

Definition

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

Examples

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

See also

Revision on June 7, 2022 at 02:50:52 by Anonymous?. See the history of this page for a list of all contributions to it.