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

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

Contents

Definition

A unital dagger 2-poset is a dagger 2-poset CC with an object 𝟙:Ob(C)\mathbb{1}:Ob(C) such that for every morphism f:Hom(𝟙,𝟙)f:Hom(\mathbb{1}, \mathbb{1}), f1 𝟙f \leq 1_\mathbb{1}, and for every object A:Ob(C)A:Ob(C), there is an onto morphism u A:A𝟙u_A:A \to \mathbb{1}.

Examples

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

See also

Revision on June 6, 2022 at 22:59:12 by Anonymous?. See the history of this page for a list of all contributions to it.