Homotopy Type Theory semiadditive dagger 2-poset > history (Rev #1)

Contents

Definition

A semiadditive dagger 2-poset is a dagger 2-poset CC such that

  • There exists an object 0:Ob(C)0:Ob(C) called the zero object such that for each object A:Ob(C)A:Ob(C), there exists a morphism Z A:Hom(0,A)Z_A:Hom(0, A) such that for each object B:Ob(C)B:Ob(C) and morphism R:Hom(A,B)R: Hom(A, B), RZ A=Z BR \circ Z_A = Z_B.

  • For each object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C), there exists a object AB:Ob(C)A \oplus B:Ob(C) called the biproduct of AA and BB, with morphisms I A:Hom(A,AB)I_A: Hom(A,A \oplus B) and I B:Hom(B,AB)I_B: Hom(B,A \oplus B), such that

    • For each object A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), and C:Ob(C)C:Ob(C) and morphism R A:Hom(A,C)R_A:Hom(A,C) and R B:Hom(B,C)R_B:Hom(B,C), there exist a morphism R:Hom(AB,C)R: Hom(A \oplus B ,C) such that RI A=R AR \circ I_A = R_A and RI B=R BR \circ I_B = R_B

    • For each object A:Ob(C)A:Ob(C), B:Ob(C)B:Ob(C), C:Ob(C)C:Ob(C), and D:Ob(C)D:Ob(C), and morphism R:Hom(A,B)R:Hom(A, B) and S:Hom(C,D)S:Hom(C,D), there exists a morphism RS:Hom(AB,CD)R \oplus S:Hom(A \oplus B,C \oplus D) where (RS) =R S (R \oplus S)^\dagger = R^\dagger \oplus S^\dagger.

Examples

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

See also

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