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

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

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 is an object|R|:Ob(C) \vert R \vert \vert:Ob(C) called and atabulation of RR and maps f:Hom(|R|,A)f:Hom(\vert R \vert, A) , andg:Hom(|R|, B A) g:Hom(\vert R \vert, B) A) , such thatR=gf g R = g \circ f^\dagger \circ g , and for every objectE:Ob(C)E:Ob(C) and maps h:Hom(E,A|R|) h:Hom(E,A) h:Hom(E,\vert R \vert) and k:Hom(E,B|R|) k:Hom(E,B) k:Hom(E,\vert R \vert), k fh h = R fk k f \circ h^\dagger h \leq = R f \circ k if and only if there exists a unique map j g : E h =|gR|k j:E g \to \circ \vert h R = \vert g \circ k such imply thath= f kj h = f k \circ j and k=gjk = g \circ j.

Properties

The category of maps of a tabular dagger 2-poset has all pullback?s.

Examples

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

See also

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