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

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



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


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 Af:Hom(|R|,A) p_A:Hom(\vert f:Hom(\vert R \vert, A) and p Bg:Hom(|R|,B) p_B:Hom(\vert g:Hom(\vert R \vert, B) such that R=p Bgp A f R = p_B g \circ p_A^\dagger f^\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.


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

See also

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