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 $C$ such that for every object $A:Ob(C)$ and $B:Ob(C)$ and morphism $R:Hom(A,B)$ , there exist is an object$|R|:\mathrm{Ob}(C)$ \vert R \vert \vert:Ob(C) called and atabulation of $R$ and maps $f:Hom(\vert R \vert, A)$ , and$g:\mathrm{Hom}(|R|,\mathrm{<span><del\; class="diffmod">\; B</del><ins\; class="diffmod">\; A</ins></span>})$ g:Hom(\vert R \vert, B) A) , such that$R=g\circ f^{†}\circ g$ R = g \circ f^\dagger \circ g , and for every object$E:Ob(C)$ and maps $h:\mathrm{Hom}(E,A|R|)$ h:Hom(E,A) h:Hom(E,\vert R \vert) and $k:\mathrm{Hom}(E,B|R|)$ k:Hom(E,B) k:Hom(E,\vert R \vert), $\mathrm{<span><del\; class="diffmod">\; k</del><ins\; class="diffmod">\; f</ins></span>}\circ h^{†}h<span><del\; class="diffmod">\; \le </del><ins\; class="diffmod">\; =</ins></span>\mathrm{<span><del\; class="diffmod">\; R</del><ins\; class="diffmod">\; f</ins></span>}\circ k$ k f \circ h^\dagger h \leq = R f \circ k if and only if there exists a unique map$\mathrm{<span><del\; class="diffmod">\; j</del><ins\; class="diffmod">\; g</ins></span>}<span><del\; class="diffmod">\; :</del><ins\; class="diffmod">\; \circ </ins></span>\mathrm{<span><del\; class="diffmod">\; E</del><ins\; class="diffmod">\; h</ins></span>}<span><del\; class="diffmod">\; \to </del><ins\; class="diffmod">\; =</ins></span>|gR\circ |k$ j:E g \to \circ \vert h R = \vert g \circ k such imply that$h=\mathrm{<span><del\; class="diffmod">\; f</del><ins\; class="diffmod">\; k</ins></span>}\circ j$ h = f k \circ j and $k = g \circ j$.

Examples

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

See also

• dagger 2-poset
• cartesian dagger 2-poset