Showing changes from revision #3 to #4:
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 functional dagger monomorphisms , , there is a functional dagger monomorphism .
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 that .
For each object , , with functional dagger monomorphisms , , there is an object with functional dagger monomorphisms , , , such that for every object with functional dagger monomorphisms , , there is a functional dagger monomorphism .
For each object , , with functional dagger monomorphisms , , there is an object with functional dagger monomorphism ,
and
The dagger 2-poset of sets and relations is a Heyting dagger 2-poset.