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

Contents

Idea

A dagger 2-poset with tabulations, such as a tabular allegory.

Definition

A tabular dagger 2-poset is a dagger 2-poset CC such that for every object A:Ob(C)A:Ob(C) and B:Ob(C)B:Ob(C) and morphism R:Hom(A,B)R:Hom(A,B) there exist an object |R|\vert R \vert called a tabulation of RR and maps p A:Hom(|R|,A)p_A:Hom(\vert R \vert, A) and p B:Hom(|R|,B)p_B:Hom(\vert R \vert, B) such that R=p Bp A R = p_B \circ p_A^\dagger, and for every object E:Ob(C)E:Ob(C) and maps h:Hom(E,A)h:Hom(E,A) and k:Hom(E,B)k:Hom(E,B), kh Rk \circ h^\dagger \leq R if and only if there exists a unique map j:E|R|j:E \to \vert R \vert such that h=fjh = f \circ j and k=gjk = g \circ j.

Examples

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

See also

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