Showing changes from revision #4 to #5:
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 for every object with and functional dagger monomorphisms ,and for every object , with functional dagger monomorphisms , there is a functional dagger monomorphism . , such that and , there is a functional dagger monomorphism such that
For each object , the identity function , is a functional dagger monomorphism, and for each object with a functional dagger monomorphism , there is trivially the same functional dagger monomorphism , such there that 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 monomorphisms monomorphism ,, , such that for every object with functional dagger monomorphisms , , there is a functional dagger monomorphism .
and
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.