Showing changes from revision #6 to #7:
Added | Removed | Changed
A Heyting dagger 2-poset is a dagger 2-poset whose category of maps is a Heyting category.
A Heyting dagger 2-poset is a dagger 2-poset such that
There is an object such that for each object , there is a functional monic map dagger monomorphism such that for each object such with that a for monic each map object , with there is a functional monic dagger map monomorphism , there such is that a functional dagger monomorphism such that .
For each object , , with functional monic dagger maps monomorphisms, , there is an object with functional monic dagger maps monomorphisms, , , such that and ,and for every object with functional monic dagger maps monomorphisms , such that and , there is a functional monic dagger map monomorphism such that
For each object , , with functional monic dagger map monomorphism, , there is an object with functional monic dagger maps monomorphisms, , , such that and , and for every object with functional monic dagger maps monomorphisms , such that and , there is a functional monic dagger map monomorphism such that .
For each object , , with functional monic dagger maps monomorphisms, , there is an object with functional monic dagger map monomorphism,
and
For each object , the identity function is a anmonic functional map, dagger monomorphism, and for each object with a functional monic dagger map monomorphism, .
The unitary isomorphism classes of functional monic dagger maps monomorphisms into every object is a Heyting algebra . Since every functional monic dagger map monomorphism is a map, thecategory of maps is a Heyting category?. As a result, Heyting dagger 2-posets are the same as division allegories and bicategories of relations.
The dagger 2-poset of sets and relations is a Heyting dagger 2-poset.