Showing changes from revision #5 to #6:
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 dagger monomorphism such that for each object with a functional dagger monomorphism , there is a functional dagger monomorphism such that .
For each object , , with functional dagger monomorphisms , , there is an object with functional dagger monomorphisms , , , such that and ,and for every object with functional dagger monomorphisms , such that and , there is a functional dagger monomorphism such that
For each object , , with functional dagger monomorphism , , there is an object with functional dagger monomorphisms , , , such that and , and for every object with functional dagger monomorphisms , such that and , there is a functional dagger monomorphism such that .
For each object , , with functional dagger monomorphisms , , there is an object with functional dagger monomorphism ,
and
For each object , the identity function is a functional dagger monomorphism, and for each object with a functional dagger monomorphism , .
The unitary isomorphism classes of functional dagger monomorphisms into every object is a Heyting algebra. Since every functional dagger monomorphism is a map, the category 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.