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

Showing changes from revision #1 to #2: Added | Removed | Changed

Contents

Idea

A dagger 2-poset whose category of maps is a cartesian monoidal category?.

Definition

A cartesian dagger 2-poset is a unital dagger 2-poset CC such that for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), Hom(A,B)Hom(A, B) is a meet-semilattice with top morphism A,B\top_{A,B} and meet operation A,B\wedge_{A,B}, and there is an object AB:Ob(C)A \otimes B:Ob(C) such that there exist maps p A:ABAp_A:A \otimes B \to A and p B:BBBp_B:B \otimes B \to B such that p B p A= A,Bp_B^\dagger \circ p_A = \top_{A,B} and u Bp B=u Ap Au_B \circ p_B = u_A \circ p_A, for every onto morphism u A:A𝟙u_A:A \to \mathbb{1} and u B:A𝟙u_B:A \to \mathbb{1}.

Examples

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

See also

Revision on April 20, 2022 at 20:54:07 by Anonymous?. See the history of this page for a list of all contributions to it.