We consider framed bicategories for which horizontal identity squares are Cartesian. We call double categories satisfying this condition regular framed bicategories. The length of a double category is a numerical invariant measuring the 'work' it takes to reconstruct the double category from its globular data. It is conjectured that framed bicategories are of length 1. In this paper we prove this conjecture for the case of regular framed bicategories.

§ INTRODUCTION

Symmetric monoidal structures on bicategories are, in some cases, more naturally expressed as horizontalizations of symmetric monoidal structures of double categories. In order to define a symmetric monoidal structure on a bicategory $B$, in the general sense of [1], it is sometimes convenient to 'lift' $B$ to a symmetric monoidal double category $C$, where the coherence equations for the symmetric monoidal structure are expressed in terms of vertical arrows of $C$. In the case in which the double category $C$ is a framed bicategory, the image of the symmetric monoidal structure on $C$, under the horizontal bicategory functor $H$, defines a symmetric monoidal bicategory structure on $B$ [2, 3]. Whether this technique can be applied to a given bicategory $B$ depends on the specifics of $B$. We are interested in the problem of establishing general criteria for when this procedure can be applied.

We consider the following problem: Given a bicategory $B$, and a category $B^*$, such that the collections of objects of $B$ and $\stB$ are equal, we wish to construct interesting double categories $C$ having $B$ as horizontal bicategory, and having $\stB$ as category of objects. Succintly $H^*C=(\stB,B)$. We say that the pair $\decB$ is a decorated bicategory and $C$ is an internalization of $\decB$. The problem of finding interesting internalizations to a given decorated bicategory $\decB$ models the case in which one wishes to define a symmetric monoidal structure on the bicategory $B$, where coherence data would be more naturally expressed in terms of a collection of vertical arrows, $\stB$. We then wish to have knowledge of the possible extensions of $B$ to double categories $C$ having $\stB$ as category of objects, i.e. $H^\ast C=\decB$. With this knowledge we would, in principle, be able to decide whether we can choose, among the internalizations of $\decB$, a framed double category where the symmetric monoidal structure we are trying to define on $B$ is naturally defined.

The problem of understanding internalizations of decorated bicategories has been considered in the series of papers [4, 5, 6], where the 2-category of double categories is fibered over a coreflective subcategory minimizing the internalization problem. This allows the definition of a numerical invariant, called the vertical length $\ell C$, associated to every double category $C$. Roughly, the number $\ell C$ measures the amount of work one would be expected to do to construct a generic square in $C$, from squares in $H^\ast C$. 1 is the minimum possible length of a double category, and the condition $\ell C=1$ roughly means that we can express squares of $C$ in terms of squares of $H^\ast C$ in a relatively straightforward way. Most framed bicategories in the literature, e.g. $\Mod,\Prof,\Bord,\Adj$ are of length 1. It is thus natural to conjecture that every framed bicategory is of length 1.

In this paper we prove a particular case of the above conjecture. We introduce the notion of regular framed bicategory: A framed bicategory is regular, if horizontal identity squares are Cartesian. Opregular framed bicategories are those for which horizontal identity squares are opcartesian. The main goal of the paper is the following Theorem.

Let $C$ be a regular/opregular framed bicategory. $\ell C=1$.

We briefly outline our strategy for proving Theorem <ref>. In [7] the notions of $\pi_2$-indexing and $\pi_2$-opindexing are introduced. A $\pi_2$-opindexing is a type of indexing associated to a decorated bicategory $\decB$, relating the arrows of $\decB$ with 2-cells of a specific type in $B$, see Section <ref>. Given a $\pi_2$-opindexing on a decorated bicategory $\decB$, a length 1 internalization $\crossb$ of $\decB$ is constructed. We associate, to every regular framed bicategory, a $\pi_2$-opindexing on $H^\ast C$, and we prove that the double category $C$ is 'parametrized' by the length 1 internalization associated to this $\pi_2$-opindexing, see Theorem <ref>. The proof o Theorem <ref> will follow almost directly from this.

We now present the contents of this paper. In Section <ref> we briefly review the notions of framed bicategory, internalization, globularly generated double category, and length. In Section <ref> we introduce regular framed bicategories, and present relevant examples. In Section <ref> we recall the definition of $\pi_2$-opindexing and the length 1 internalization associated to a $\pi_2$-opindexing. In Section <ref> we present the arguments for our proof of Theorem <ref>. We associate $\pi_2$-opindexings to regularly framed bicategories, and we prove Theorem <ref> relating regular framed bicategories and length 1 internalizations of $\pi_2$-opindexings. The argument for the proof of Theorem <ref> will follow from this.

§ PRELIMINARIES

§.§ Double categories

We will write $C_0,C_1$ for the category of objects and the category of morphisms of a double category $C$; $L,R$ for the left and right frame functors of $C$, and $U$ for the unit (horizontal identity) functor of $C$. Following [3] we will write $\boxminus,\boxvert$ for the vertical and horizontal composition operations of $C$ respectively. We will represent squares in double categories as diagrams of the form:

every picture/.style=line width=0.75pt

(240.73,120.3) – (300.9,120.3) – (300.9,180.47) – (240.73,180.47) – cycle ;

(263.92,144.91) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi $;

(225.07,145.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(306.64,144.91) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(265,105) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(265.92,185.26) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(225.07,113.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $a$;

(225.07,174.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $c$;

(305.07,174.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $d$;

(306.07,113.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $b$;

where squares are read from left to right and from top to bottom, i.e. the edges $f,g$ are the left and right frame of the square $\varphi$, while the edges $\alpha,\beta$ are the vertical domain and codomain of $\varphi$ respectively. We represent (horizontal or vertical) identities as red edges. We represent horizontal identity squares as squares marked with the letter $U$:

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300.07,139.3) – (360.23,139.3) ;

(300.07,139.3) – (300.07,199.47) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (299.73,199.13) – (359.9,199.13) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (359.9,138.97) – (359.9,199.13) ;

(284,161.07) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(364,161.73) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(324,166.83) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

An important class of squares is the collection squares of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320.07,159.3) – (380.23,159.3) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320.07,159.3) – (320.07,219.47) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (319.73,219.13) – (379.9,219.13) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (379.9,158.97) – (379.9,219.13) ;

We will write $\pi_2(C,a)$ for the set of all such squares with vertex $a$. By the Eckmann-Hilton argument, the horizontal composition and the vertical composition of such squares coincide and are commutative. The set $\pi_2(C,a)$ is thus a commutative monoid. Globular squares are represented by diagrams of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300.07,119.3) – (360.23,119.3) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300.07,119.3) – (300.07,179.47) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (299.73,179.13) – (359.9,179.13) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (359.9,118.97) – (359.9,179.13) ;

The collection of globular squares of a double category $C$ forms a bicategory $HC$, the horizontal bicategory of $C$. Bicategories are precisely the double categories whose squares are all globular.

§.§ Framed bicategories

A framed bicategory is a double category such that the left-right frame functor $L\times R:C_1\to C_0^2$ is a bifibration. See [2, 3]. The condition of a double category $C$ being a framed bicategory provides extension and restriction of horizontal arrows along vertical arrows. In a framed bicategory $C$, given a hollow niche

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (241,190.6) – (291,190.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (241,140.6) – (241,190.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (291,140.6) – (291,190.6) ;

(221.6,158) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(297.6,158.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(260.8,192.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

there exists a Cartesian square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (261,210.6) – (311,210.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (261,160.6) – (261,210.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (311,160.6) – (311,210.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (261,160.6) – (311,160.6) ;

(241.6,178) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(317.6,178.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(280.8,212.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(271.47,142.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $f^{\ast } \alpha g^{\ast }$;

(274.33,179.67) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Cart;

filling the niche. A Cartesian square, as above, provides a way of changing basis for the horizontal morphism $\alpha$ along restriction with respect to the vertical morphisms $f$ and $g$. Given a Cartesian square as above, every other square of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (261,179.6) – (311,179.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (261,129.6) – (261,179.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (311,129.6) – (311,179.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (261,129.6) – (311,129.6) ;

(241.6,147) node [anchor=north west][inner sep=0.75pt]  [font=]  $fh$;

(317.6,147.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $gk$;

(280.8,181.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(281.47,112.73) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(278.61,149.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi $;

factors uniquely as

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281,199.6) – (331,199.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281,149.6) – (281,199.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (331,149.6) – (331,199.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281,149.6) – (331,149.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281.02,99.65) – (281.02,149.65) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (331.02,99.65) – (331.02,149.65) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281.02,99.65) – (331.02,99.65) ;

(265.14,167.31) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(337.6,167.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(300.8,201.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(300.85,83.19) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(294.33,168.67) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Cart;

(264.22,119.02) node [anchor=north west][inner sep=0.75pt]  [font=]  $h$;

(336.52,118.25) node [anchor=north west][inner sep=0.75pt]  [font=]  $k$;

(298.24,119.78) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Psi $;

for some uniquely determined square $\Psi$. In particular, every square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281,199.6) – (331,199.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281,149.6) – (281,199.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (331,149.6) – (331,199.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281,149.6) – (331,149.6) ;

(265.6,167) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(336.6,167.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(300.8,201.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(301.47,132.73) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(298.61,169.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi $;

Factors uniquely as

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,219.2) – (351,219.2) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,169.2) – (301,219.2) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (351,169.2) – (351,219.2) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,169.2) – (351,169.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (301.02,119.25) – (301.02,169.25) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (351.02,119.25) – (351.02,169.25) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301.02,119.25) – (351.02,119.25) ;

(285.14,186.91) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(357.6,186.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(320.8,221.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(320.85,102.79) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(314.33,188.27) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Cart;

(318.24,139.38) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Psi $;

A choice of cartesian squares for niches as above is a cleavage for $L\times R$. In case a cleavage for $L\times R$ has been chosen, we will say that $L\times R$ is a cloven fibration. A cloven fibration is normal if the square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (180,180.6) – (230,180.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (180,230.6) – (230,230.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (180,180.6) – (180,230.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (230,180.6) – (230,230.6) ;

(189.69,165.71) node [anchor=north west][inner sep=0.75pt]  [font=]  $1^{*} \alpha 1^{\ast }$;

(201.36,232.71) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(192.67,200.33) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Cart;

is the horizontal identity square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (160,160.6) – (210,160.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (160,210.6) – (210,210.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (160,160.6) – (160,210.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (210,160.6) – (210,210.6) ;

(178.69,145.71) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(179.36,212.71) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(177.36,180.37) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

and is split if the Cartesian square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (200,200.6) – (250,200.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (200,250.6) – (250,250.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (200,200.6) – (200,250.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (250,200.6) – (250,250.6) ;

(196.69,182.71) node [anchor=north west][inner sep=0.75pt]  [font=]  $( fh)^{*} \alpha ( gk)^{\ast }$;

(221.36,252.71) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(212.67,220.33) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Cart;

(255.36,218.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $gk$;

(182.76,218) node [anchor=north west][inner sep=0.75pt]  [font=]  $fh$;

is the composite

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,219.6) – (351,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,169.6) – (301,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (351,169.6) – (351,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,169.6) – (351,169.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301.02,119.65) – (301.02,169.65) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (351.02,119.65) – (351.02,169.65) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301.02,119.65) – (351.02,119.65) ;

(285.14,187.31) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(357.6,187.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(320.8,221.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(314.33,188.67) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Cart;

(284.22,139.02) node [anchor=north west][inner sep=0.75pt]  [font=]  $h$;

(356.52,138.25) node [anchor=north west][inner sep=0.75pt]  [font=]  $k$;

(314.33,139.33) node [anchor=north west][inner sep=0.75pt]  [font=] [align=left] Cart;

(298,100.11) node [anchor=north west][inner sep=0.75pt]  [font=]  $( fh)^{*} \alpha ( gk)^{\ast }$;

§.§ Globularly generated double categories

A decoration of a bicategory $B$ is a category $B^\ast$ having the same collection of objects as $B$. If $B^\ast$ is a decoration of $B$ we say that $\decB$ is a decorated bicategory. The pair $(C_0,HC)$ is a decorated bicategory for every double category $C$. We write $H^*C$ for this decorated bicategory, and we call it the decorated horizontalization of $C$. We are interested in the following problem:

Let $\decB$ be a decorated bicategory. Find double categories $C$ satisfying the equation $H^*C=\decB$.

We understand problem <ref> as the problem of lifting a bicategory $B$ to a double category through an orthogonal direction, provided by $\stB$. A solution to Problem <ref> for a decorated bicategory $\decB$ will be called an internalization of $B$. Globularly generated double categories were introduced in [4] as minimal solutions to Problem <ref>. A double category $C$ is globularly generated if $C$ is generated, as a double category, by its collection of globular squares. Pictorially a double category $C$ is globularly generated if every square of $C$ can be written as vertical and horizontal compositions of squares of the form:

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (230.07,140.3) – (290.23,140.3) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (230.07,140.3) – (230.07,200.47) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (229.73,200.13) – (289.9,200.13) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (289.9,139.97) – (289.9,200.13) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (330.73,139.97) – (390.9,139.97) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (330.73,139.97) – (330.73,200.13) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (330.4,199.8) – (390.57,199.8) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (390.57,139.63) – (390.57,199.8) ;

(354,164.07) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

Given a double category $C$ we write $\gamma C$ for the sub-double category of $C$ generated by squares of the above form. We call $\gamma C$ the globularly generated piece of $C$. $\gamma C$ is globularly generated, satisfies the equation

\[H^*C=H^*\gamma C\]

and is contained in every sub-double category $D$ of $C$ satisfying the equation $H^*C=H^*D$. Moreover, a double category $C$ is globularly generated if and only if $C$ does not contain proper sub-double categories satisfying the above equation. Globularly generated double categories are thus minimal with respect to $H^*$. See [6] for a functorial version of this statement.

§.§ Length 1

Globularly generated double categories admit a helpful combinatorial description provided in the form of a filtration of their categories of squares. This defines a numberical invariant which we call the length. In this note we will only be interested in length 1 double categories. We refer the reader to <cit.> for a general treatment. A globularly generated double category $C$ is of length 1, $\ell C=1$ in symbols, if every square in $C$ admits an expression as vertical composition of squares of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (230.07,140.3) – (290.23,140.3) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (230.07,140.3) – (230.07,200.47) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (229.73,200.13) – (289.9,200.13) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (289.9,139.97) – (289.9,200.13) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (330.73,139.97) – (390.9,139.97) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (330.73,139.97) – (330.73,200.13) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (330.4,199.8) – (390.57,199.8) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (390.57,139.63) – (390.57,199.8) ;

(354,164.07) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

i.e. if every square in $C$ is a vertical composite of horizontal identity and globular squares. More geometrically, if we regard the globular squares and horizontal identities of a double category $C$ as the simplest possible squares of $C$, then it is natural to represent globular and horizontal identity squares as squares marked by 0, i.e. as:

every picture/.style=line width=0.75pt

(292.77,151.6) – (369.82,151.6) – (369.82,228.65) – (292.77,228.65) – cycle ;

(324.95,185.52) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

A trivial, but important observation is that the collection of 0-marked squares is closed under horizontal composition. $C$ is of length 1 if every square in $C$ can be represented geometrically as:

every picture/.style=line width=0.75pt

(290.34,171.28) – (369.16,171.28) – (369.16,250.09) – (290.34,250.09) – cycle ;

(290.41,190.71) – (369.3,190.41) ;

(290.64,210.71) – (368.86,210.66) ;

(290.19,230.49) – (369.3,230.41) ;

(324.45,177.54) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(324.34,195.76) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(323.9,236.43) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(333.41,211.46) node [anchor=north west][inner sep=0.75pt]  [font=,rotate=-90.3,xscale=0.9,yscale=0.9]  $\cdots $;

In general, given two horizontally composable squares admitting subdivisions as above $\varphi,\psi$, it might be the case that for every choice of vertical subdivision of $\varphi$ and $\psi$ into marked 0 squares, the horizontal composition $\varphi\boxbar\psi$ looks like

every picture/.style=line width=0.75pt

(271.59,161) – (350.41,161) – (350.41,239.82) – (271.59,239.82) – cycle ;

(271.66,180.43) – (350.55,180.14) ;

(271.89,197.58) – (350.11,197.53) ;

(271.44,220.21) – (350.55,220.14) ;

(351.09,161) – (429.91,161) – (429.91,239.82) – (351.09,239.82) – cycle ;

(351.16,190.15) – (430.27,190.7) ;

(349.8,211.35) – (429.85,211.23) ;

(305.7,167.26) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(305.59,183.48) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(305.15,226.15) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(314.66,201.18) node [anchor=north west][inner sep=0.75pt]  [font=,rotate=-90.3,xscale=0.9,yscale=0.9]  $\cdots $;

(384.63,171.83) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(385.22,222.15) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(394.44,192.61) node [anchor=north west][inner sep=0.75pt]  [font=,rotate=-90.3,xscale=0.9,yscale=0.9]  $\cdots $;

See <cit.> for an explicit example. $C$ is of length 1, precisely when the above does not happen, i.e. when given two horizontally compatible squares $\varphi,\psi$ admitting decompositions as vertical compositions of squares marked with 0, then we can always find vertical subdivisions making $\varphi\boxbar\psi$ look like:

every picture/.style=line width=0.75pt

(251.59,141) – (330.41,141) – (330.41,219.82) – (251.59,219.82) – cycle ;

(251.66,160.43) – (330.55,160.14) ;

(251.89,180.43) – (330.11,180.38) ;

(251.44,200.21) – (330.55,200.14) ;

(331.09,141) – (409.91,141) – (409.91,219.82) – (331.09,219.82) – cycle ;

(331.16,160.43) – (410.05,160.14) ;

(331.39,180.43) – (409.61,180.38) ;

(330.94,200.21) – (410.05,200.14) ;

(285.7,147.26) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(285.59,165.48) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(285.15,206.15) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(294.66,181.18) node [anchor=north west][inner sep=0.75pt]  [font=,rotate=-90.3,xscale=0.9,yscale=0.9]  $\cdots $;

(365.2,147.26) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(365.09,165.48) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(364.65,206.15) node [anchor=north west][inner sep=0.75pt]  [font=,xscale=0.9,yscale=0.9]  $0$;

(374.16,181.18) node [anchor=north west][inner sep=0.75pt]  [font=,rotate=-90.3,xscale=0.9,yscale=0.9]  $\cdots $;

In that case we can use the exchange identity to re-arrange the above composition into a vertical subdivision of 0-marked squares. Squares in a globularly generated double category of length 1 thus admit a simple expression in terms of globular and unit squares. It is thus desirable to have criteria for knowing when a given double category is of length 1.

§.§ Assumptions

We will assume, for the rest of the paper, that all double categories are strict, i.e. we will assume that horizontal composition is associative on the nose, and that unit squares act as units with respect to horizontal composition strictly. We will thus only consider decorated 2-categories and not general decorated bicategories. Finally, we will assume, throughout the paper, that framed bicategories $C$ are such that $L\times R$ is a normal, cloven fibration.

§ REGULAR FRAMED BICATEGORIES

Let $C$ be a framed bicategory. We will say that $C$ is regular, if for every morphism $f$ in $C_0$, the horizontal identity square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (281,180.6) – (331,180.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (281,230.6) – (331,230.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281,180.6) – (281,230.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (331,180.6) – (331,230.6) ;

(267.14,201.26) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(337.71,201.26) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(300.29,202.11) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

is Cartesian. If every horizontal identity as above is opCartesian, we will say that $C$ is opregular. If a framed bicategory is both regular and opregular we will say that it is biregular.

We will mostly treat regular framed bicategories in this note, but the arguments and results for opregular framed bicategories are analogous.

In a regular framed bicategory, every square of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (281,199.6) – (331,199.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281,149.6) – (281,199.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (331,149.6) – (331,199.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (281,149.6) – (331,149.6) ;

(261.6,167) node [anchor=north west][inner sep=0.75pt]  [font=]  $fh$;

(337.6,167.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $fk$;

(301.47,132.73) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(298.61,169.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi $;

can be factored uniquely as

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (301,219.6) – (351,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,169.6) – (301,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (351,169.6) – (351,219.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (301,169.6) – (351,169.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301.02,119.65) – (301.02,169.65) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (351.02,119.65) – (351.02,169.65) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301.02,119.65) – (351.02,119.65) ;

(285.14,187.31) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(357.6,187.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(320.85,103.19) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(284.22,139.02) node [anchor=north west][inner sep=0.75pt]  [font=]  $h$;

(356.52,138.25) node [anchor=north west][inner sep=0.75pt]  [font=]  $k$;

(318.24,139.78) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Psi $;

(319.24,190.78) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

In particular, every square of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (301,219.6) – (351,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,169.6) – (301,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (351,169.6) – (351,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,169.6) – (351,169.6) ;

(284.6,187) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(357.6,187.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(321.47,152.73) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(318.61,189.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi $;

admits a unique representation as a vertical composite of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (321,239.6) – (371,239.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (321,189.6) – (321,239.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (371,189.6) – (371,239.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (321,189.6) – (371,189.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (321.02,139.65) – (321.02,189.65) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (371.02,139.65) – (371.02,189.65) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (321.02,139.65) – (371.02,139.65) ;

(305.14,207.31) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(377.6,207.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(340.85,123.19) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(338.24,159.78) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Psi $;

(339.24,210.78) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

Let $C$ be a framed bicategory. Let $f$ be a vertical isomorphism in $C$. The horizontal identity square $U_f$ is Cartesian. In particular, if $C_0$ is a groupoid, then $C$ is regular framed.

Let $f$ be a vertical isomorphism. The horizontal identity $U_f$ is a vertical isomorphism square. By <cit.>, $U_f$ is Cartesian.

By Proposition <ref>, the double category $\Bord_n$ of $n$-dimensional bordisms is a regular framed bicategory. Every double groupoid with connections [8], and in particular the homotopy doule groupoid $\rhoX$, of a topological space $X$, is also a regular framed bicategory.

The framed bicategory $\Span$ is a framed bicategory that is not regular. We can show this directly through an example of a square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (261,160.6) – (311,160.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (261,210.6) – (311,210.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (261,160.6) – (261,210.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (311,160.6) – (311,210.6) ;

(242.29,178.83) node [anchor=north west][inner sep=0.75pt]  [font=]  $fh$;

(315.71,178.83) node [anchor=north west][inner sep=0.75pt]  [font=]  $fk$;

that does not admit a factorization of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (301,219.6) – (351,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,169.6) – (301,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (351,169.6) – (351,219.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,169.6) – (351,169.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301.02,119.65) – (301.02,169.65) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (351.02,119.65) – (351.02,169.65) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301.02,119.65) – (351.02,119.65) ;

(285.14,187.31) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(357.6,187.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(284.22,139.02) node [anchor=north west][inner sep=0.75pt]  [font=]  $h$;

(356.52,138.25) node [anchor=north west][inner sep=0.75pt]  [font=]  $k$;

(320,189.11) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

along the corresponding horizontal identity square. Consider a non-commutative rhombus of the form

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]

T      S

[->,font=,>=angle 90]
(m-1-2) edge node [left]$u$ (m-2-1)
edge node [right]$v$ (m-2-3)
(m-2-1) edge node [left]$h$(m-3-2)
(m-2-3) edge node [right]$k$(m-3-2)

where e.g. $W,T,X$ are equal to $\{\ast.\ast'\}$, $S$ is the terminal set $\{\ast\}$, $u,h$ are identities, an $k$ is any of the two possible functions $S\to X$. If we make $Y$ be the terminal set $\{\ast\}$, and let $f:X\to Y$ the unique function from $X$ to $Y$. The diagram

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]

T      S

[->,font=,>=angle 90]
(m-1-2) edge node [left]$u$ (m-2-1)
edge node [right]$v$ (m-2-3)
(m-2-1) edge node [left]$h$(m-3-2)
(m-2-3) edge node [right]$k$(m-3-2)
(m-3-2)edge node [right]$f$(m-4-2)

is commutive, where the left and right boundaries of the diagram are both equal to $f$. The diagram

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
Z   W   Z

Y   Y   Y
[->,font=,>=angle 90]
(m-1-2) edge node [above]$u$ (m-1-1)
edge node [above]$v$ (m-1-3)
(m-1-1) edge node [left]$fh$(m-2-1)
(m-1-2) edge node [right]$\varphi$(m-2-2)
(m-1-3)edge node [right]$fk$(m-2-3)
(m-2-2) edge [red]node [black,below]$id$(m-2-1)
(m-2-2)edge [red]node [black,below]$id$(m-2-3)

is thus a square in $\Span$, the fact the the inner rhombus above does not commute, says that there does not exist a factorization of the above square as a vertical composite of the form

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
Z   W   Z

X   X   X

Y   Y   Y
[->,font=,>=angle 90]
(m-1-2) edge node [above]$u$ (m-1-1)
edge node [above]$v$ (m-1-3)
(m-1-1) edge node [left]$h$(m-2-1)
(m-1-2) edge node [right]$\psi$(m-2-2)
(m-1-3)edge node [right]$k$(m-2-3)
(m-2-2) edge [red]node [black,below]$id$(m-2-1)
(m-2-2)edge [red]node [black,below]$id$(m-2-3)

(m-2-2) edge node [right]$f$(m-3-2)
(m-2-3) edge node [right]$f$(m-3-3)
(m-2-1) edge node [left]$f$(m-3-1)
(m-3-2) edge [red]node [black,below]$id$(m-3-1)
(m-3-2)edge [red]node [black,below]$id$(m-3-3)

for some function $\psi$, and thus the bottom square, i.e., the horizontal identity square $U_f$ is not Cartesian. We conclude that $\Span$ is not regular. Similar arguments prove that neither $\Rel$ nor $\Mod$ are regular.

Let $C$ be a framed bicategory. Let $C^\ast$ be the sub-double category whose squares are

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,200.6) – (351,200.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,250.6) – (351,250.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (301,200.6) – (301,250.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (351,200.6) – (351,250.6) ;

(288.14,221.26) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(357.71,221.26) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(320.29,222.11) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(322.21,257.26) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(319.96,188.76) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

in $C$, where vertical arrows $f$ and $g$ are isomorphisms. $C^\ast$ is also a framed bicategory. Moreover, by Proposition <ref>, $C^\ast$ is regular. The double categories $\Span ^\ast,\Mod ^\ast$, and $\Rel ^\ast$ are thus regular framed bicategories. Observe that in order to define a symmetric monoidal bicategory through a framed bicategory lift $C$ as in [2], the only vertical arrows that we need are the invertible ones, and thus the arrows of $C^\ast$.

The following is an example of a regular framed bicategory $C$ for which the category of objects $C_0$ is not a groupoid. This example is due to Robert Paré.

Let $\Eq$ be the double category whose squares are of the form

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
C   D

C'   D'
[->,font=,>=angle 90]
(m-1-1) edge node [above]$K$ (m-1-2)
edge node [left]$F$ (m-2-1)
(m-1-2) edge node [right]$G$(m-2-2)
(m-2-1) edge node [below]$K'$(m-2-2)
(m-1-1)edge[white] node [black]$\Downarrow$(m-2-2)

where $C,C',D,D'$ are categories, $F,G$ are equivalences, and $H,K$ are functors that are not-necessarily equivalences. We show that $\Eq$ is a regular framed bicategory. We first show that $\Eq$ is a framed bicategory. Let $F:C\to C'$ be an equivalence. Let $F^{-1}:C'\to C$ be such that $F^{-1}F\cong id_C$ and $FF^{-1}\cong id_{C'}$. Moreover, choose natural isomorphisms $\eta:F^{-1}F\Rightarrow id_C$ and $\epsilon: FF^{-1}\Rightarrow id_{C'}$ such that $(F,F^{-1},\eta,\epsilon)$ is an adjoint equivalence. The squares

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
C   D      C   D

D   D      C   C

C   C      C   C

D   C      C   D
[->,font=,>=angle 90]
(m-1-1) edge node [above]$F$ (m-1-2)
edge node [left]$F$ (m-2-1)
(m-1-2) edge [red]node [black,right](m-2-2)
(m-2-1) edge [red]node [black,below](m-2-2)
(m-1-1)edge[white] node [red]$=$(m-2-2)

(m-1-4) edge node [above]$F^{-1}$ (m-1-5)
edge [red] node [black,left] (m-2-4)
(m-1-5) edge node [right]$F$(m-2-5)
(m-2-4) edge [red]node [black](m-2-5)
(m-1-4)edge[white] node [black]$ \eta$(m-2-5)

(m-4-1) edge[red] node [black] (m-4-2)
edge node [left]$F$ (m-5-1)
(m-4-2) edge [red]node [black,right](m-5-2)
(m-5-1) edge node [below]$F^{-1}$(m-5-2)
(m-4-1)edge[white] node [black]$\epsilon^{-1}$(m-5-2)

(m-4-4) edge [red]node [,black,above] (m-4-5)
edge [red] node [black,left] (m-5-4)
(m-4-5) edge node [right]$F$(m-5-5)
(m-5-4) edge node [below]$F$(m-5-5)
(m-4-4)edge[white] node [red]$=$(m-5-5)

are a set of companions and conjoints for $F$. This follows directly from the condition that $(F,F^{-1},\eta,\epsilon)$ is an adjoint equivalence. A cartesian square for the niche

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
C   C

D   D
[->,font=,>=angle 90]
(m-1-1) edge node [left]$F$ (m-2-1)
(m-1-2) edge node [right]$F$(m-2-2)
(m-2-1) edge [red] node [](m-2-2)

can be constructed as the horizontal composite

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
C   D   D   C

D   D   D   D
[->,font=,>=angle 90]
(m-1-1) edge node [above]$F$ (m-1-2)
(m-1-2) edge [red]node [right](m-1-3)
(m-1-3) edge node [above]$F^{-1}$(m-1-4)
(m-1-1) edge [white]node [red]$=$ (m-2-2)

(m-1-1) edge node [left]$F$ (m-2-1)
(m-1-2) edge [red]node [](m-2-2)
(m-1-3) edge [red]node [](m-2-3)
(m-1-4) edge node [right]$F$(m-2-4)
(m-1-3) edge [white]node [black]$\eta$(m-2-4)

(m-2-1) edge[red] node[]  (m-2-2)
(m-2-2) edge[red] node[](m-2-3)
(m-2-3) edge[red] node[](m-2-4)

see <cit.>. The above composite is

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
C   C

D   D
[->,font=,>=angle 90]
(m-1-1) edge node [above]$FF^{-1}$ (m-1-2)
edge node [left]$F$ (m-2-1)
(m-1-2) edge node [right]$F$(m-2-2)
(m-2-1) edge[red] node [](m-2-2)
(m-1-1)edge[white] node [black]$F\eta$(m-2-2)

The globular square

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
C   C

C   C
[->,font=,>=angle 90]
(m-1-1) edge[red] node  (m-1-2)
edge[red] node  (m-2-1)
(m-1-2) edge[red] node (m-2-2)
(m-2-1) edge node [below]$FF^{-1}$(m-2-2)
(m-1-1)edge[white] node [black]$\eta^{-1}$(m-2-2)

is an isomorphism. The composite square

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
C   C

C   C

D   D
[->,font=,>=angle 90]
(m-1-1) edge[red] node  (m-1-2)
edge[red] node  (m-2-1)
(m-1-2) edge[red] node (m-2-2)
(m-2-1) edge node [below]$FF^{-1}$(m-2-2)
(m-1-1)edge[white] node [black]$\eta^{-1}$(m-2-2)

(m-2-1) edge node [left]$F$ (m-3-1)
(m-2-2) edge node [right]$F$(m-3-2)
(m-3-1) edge[red] node [](m-3-2)
(m-2-1)edge[white] node [black]$F\eta$(m-3-2)

is thus also a a Cartesian square. The above composite is equal to the horizontal identity square

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
C   C

C   C
[->,font=,>=angle 90]
(m-1-1) edge[red] node  (m-1-2)
edge[] node[left] $F$ (m-2-1)
(m-1-2) edge[] node[right] $F$(m-2-2)
(m-2-1) edge [red]node [](m-2-2)
(m-1-1)edge[white] node [black]$U$(m-2-2)

We conclude that $\Eq$ is a regular framed bicategory. A construction similar to $\Eq$ can be performed for every 2-category $B$, defining a double category of equivalences in $B$. The same arguments as above would prove that this is always a regular framed bicategory.

§ $\PI_2$-INDEXINGS AND LENGTH 1 INTERNALIZATIONS

In this section we recall the definition of $\pi_2$-indexings and $\pi_2$-opindexings on a decorated bicategory $\decB$, and the construction of the globularly generated internalization $\crossb$.

Let $(B^*,B)$ be a decorated 2-category. A $\pi_2$-indexing on $(B^*,B)$ is a functor

\[\indFunct\]

such that for every object $a$ in $\stB$, the monoid $\Phi(a)$ is the commutative monoid $\pi_2(B,a)$ of a, in $B$. A $\pi_2$-opindexing on $(B^*,B)$ is an indexing on $(B^{\ast op},B)$.

Examples of $\pi_2$-indexings and $\pi_2$-opindexings can be found in [7]. Our main interest on $\pi_2$-indexings comes from the following result.

Let $\decB$ be a decorated 2-category. For every $\pi_2$-indexing or $\pi_2$-opindexing $\Phi$ on $\decB$, there exists an internalization $\crossb$ of $\decB$ such that $\ell\crossb=1$.

We briefly review the construction of the double category $\crossb$ from the data of a $\pi_2$-opindexing appearing in Theorem <ref>. Squares in $\crossb$ are either 2-cells in $B$ or triples of the form $(\varphi_\downarrow,f,\varphi_\uparrow)$ where $f:a\to b$ is a morphism in $C_0$, and $\varphi_\downarrow,\varphi_\uparrow$ are 2-cells in $B$ of the form $\varphi_\uparrow:\alpha\Rightarrow id_a$ and $\varphi_\downarrow:id_v\Rightarrow \beta$ for 1-cells $\alpha:a\to a$ and $\beta:b\to b$ in $B$. We identify triples of the form $(\varphi_\downarrow,id,\varphi_\uparrow)$ with 2-cells $\varphi_\downarrow\boxminus \varphi_\uparrow$ in $B$. Given a morphism $f$ in $B^\ast$, the horizontal identity square $U_f$ in $\crossb$ is the square $(id,f,id)$. Moreover, we can identify the 2-cells $\varphi_\downarrow$ and $\varphi_\uparrow$ with $(\varphi_\downarrow,id,id)$ and $(id,id,\varphi_\uparrow)$. Thus, geometrically, a triple $(\varphi_\downarrow,f,\varphi_\uparrow)$ can be identified with a vertical composition of the form $\varphi_\downarrow\boxminus U_f\boxminus \varphi_\uparrow$. Every nonglobular square $\varphi$ in $\crossb$ can thus be represented as a composite of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,69.4) – (350,69.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,119.4) – (350,119.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,69.4) – (300,119.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,69.4) – (350,119.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,119.4) – (300,169.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (350,119.4) – (350,169.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,169.4) – (350,169.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,219) – (350,219) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,169) – (300,219) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,169) – (350,219) ;

(352.36,135.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(289.36,134.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(318.36,185.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow }$;

(318.21,137.5) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(317.96,84.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\uparrow }$;

Warning: Whenever the vertical morphism $f$ is not trivial, the decomposition of $(\varphi_\downarrow,f,\varphi_\uparrow)$ as a composite of squares $\varphi_\downarrow,U_f$ and $\varphi_\uparrow$ above is unique, compare with Example <ref>. Since this is not the case in general, we will avoid, in this note, representing squares in $\crossb$ geometrically as above. Note however that squares in a double category admitting a decomposition as a vertical composite as above, are called squares in canonical form in [7], and that double categories where every length 1 square admits a decomposition in canonical form, is of length 1. This will be crucial in the argument of Theorem <ref>.

Given horizontally composable squares $\varphi=(\varphi_\downarrow,f,\varphi_\uparrow)$ and $\psi=(\psi_\downarrow,f,\psi_\uparrow)$, the horizontal composition $\psi\boxbar\varphi$ is then the triple $(\psi_\downarrow\boxbar\varphi_\downarrow,f,\psi_\uparrow\boxbar\varphi_\uparrow)$. The structure provided by $\Phi$ comes into play in the vertical composition of squares. Two squares  $\varphi=(\varphi_\downarrow,f,\varphi_\uparrow)$ and $\psi=(\psi_\downarrow,g,\psi_\uparrow)$ in $\crossb$ are vertically composable if and only if $\varphi_\downarrow$ and $\psi_\uparrow$ are vertically composable, i.e. if we can form the vertical composition $\psi_\uparrow\boxminus\varphi_\downarrow$ in $B$. In that case $\psi\boxminus\varphi$ is defined using a 'middle Grothendieck construction composition' as the square $(\psi_\downarrow\boxminus \Phi_g(\psi_\uparrow\boxminus\varphi_\downarrow),gf,\varphi_\downarrow)$. For a precise form of the construction appearing in Theorem <ref> see [7]. A geometric interpretation of the above construction will be the basis for our proof of theorem <ref>.

constructed as follows: First consider triples of the form $(\varphi_\downarrow,f,\varphi_\uparrow)$, where $f:a\to b$ is a morphism in $\decB$, and where $\varphi_\downarrow$ and $\varphi_\uparrow$ are 2-cells in $B$ of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (320,89.4) – (370,89.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,139.4) – (370,139.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,89.4) – (320,139.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (370,89.4) – (370,139.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (420.4,90.6) – (470.4,90.6) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (420.4,140.2) – (470.4,140.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (420.4,90.2) – (420.4,140.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (470.4,90.2) – (470.4,140.2) ;

(438.76,106.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow }$;

(337.96,104.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\uparrow }$;

(339.56,76.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(439.56,142.4) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

for some horizontal arrows $\alpha,\beta$. We would like to consider triples $(\varphi_\downarrow,f,\varphi_\uparrow)$ as above as the squares with boundary

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (340,109.4) – (390,109.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (340,159.4) – (390,159.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (340,109.4) – (340,159.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (390,109.4) – (390,159.4) ;

(359.56,95.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $\alpha $;

(360.76,160.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $\beta $;

(327.16,129.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(392.76,127.6) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

i.e. with $f$ as left and right frame, and with domain and codomain of $\varphi_\uparrow$ and $\varphi_\downarrow$ as vertical domain and codomain respectively. In that case, 2-cells in $B$ would be precisely the triples of the form $(\varphi_\downarrow,id,\varphi_\uparrow)$. Notice that under the above identification these would be the 2-cells in $B$ admitting a vertical composition

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (340,109.4) – (390,109.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (340,159.4) – (390,159.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (340,109.4) – (340,159.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (390,109.4) – (390,159.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (340.2,60) – (390.2,60) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (340.2,59.6) – (340.2,109.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (390.2,59.6) – (390.2,109.6) ;

(358.56,76.04) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\uparrow }{}$;

(357.96,124.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow }$;

into a red square. Not all 2-cells in $B$ admit such decomposition, and thus we add all 2-cells of $B$ to squares of the form $(\varphi_\downarrow,f,\varphi_\uparrow)$ through a pushout of categories. We thus obtain squares that are either globular, identified with 2-cells in $B$ or new squares of the form $(\varphi_\downarrow,f,\varphi_\uparrow)$, withe the condition that a square of the second form identifies with the corresponding 2-cell in $B$ if its globular. The condition that $B$ should be contained in $\crossb$ as a vertically trivial double subcategory determines the operations on globular 2-cells in $\crossb$. Given a morphism $f$ in $B^\ast$, the horizontal identity square $U_f$ in $\crossb$ is the square $(id,f,id)$. Given horizontally composable squares $\varphi=(\varphi_\downarrow,f,\varphi_\uparrow)$ and $\psi=(\psi_\downarrow,f,\psi_\uparrow)$, the horizontal composition $\psi\boxbar\varphi$ is then the triple $(\psi_\downarrow\boxbar\varphi_\downarrow,f,\psi_\uparrow\boxbar\varphi_\uparrow)$. Finally, two squares  $\varphi=(\varphi_\downarrow,f,\varphi_\uparrow)$ and $\psi=(\psi_\downarrow,g,\psi_\uparrow)$ are vertically composable if and only if $\varphi_\downarrow$ and $\psi_\uparrow$ are composable, i.e. if we can form the following vertical composition of 2-cells

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (360,129.4) – (410,129.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (360,179.4) – (410,179.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (360,129.4) – (360,179.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (410,129.4) – (410,179.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (360.2,80) – (410.2,80) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (360.2,79.6) – (360.2,129.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (410.2,79.6) – (410.2,129.6) ;

(378.56,96.04) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow }{}$;

(377.96,144.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\psi _{\uparrow }$;

In that case $\psi\boxminus\varphi$ is the square $(\psi_\downarrow\boxminus \Phi_g(\psi_\uparrow\boxminus\varphi_\downarrow),gf,\varphi_\downarrow)$. Say more about how the opindexing plays here, and also about how decompositions as above are unique

§ REGULAR FRAMED BICATEGORIES ARE OF LENGTH 1

In this section we present a proof of Theorem <ref>. The construction appearing in Theorem <ref> will play a crucial role. We begin by proving the following lemma, in which a $\pi_2$-opindexing is associated to every regular framed bicategory.

Let $C$ be a regular framed bicategory. Let $f:a\to b$ be a vertical morphism in $C$. If for every $\varphi\in\pi_2(C,b)$ we write $\Phi_f(\varphi)$ for the unique square in $\pi_2(C,a)$ appearing in the factorization of

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (220.67,90) – (270.67,90) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (220.67,140) – (270.67,140) ;

(220.67,90) – (220.67,140) ;

(270.67,90) – (270.67,140) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (220.67,190) – (270.67,190) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (220.67,140) – (220.67,190) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (270.67,140) – (270.67,190) ;

(273.03,108.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(210.03,108.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(241.28,157.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi $;

(238.28,113.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

as a vertical composition

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (330,139.67) – (380,139.67) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (330,89.33) – (380,89.33) ;

(330,139.67) – (330,189.67) ;

(380,139.67) – (380,189.67) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (330,189.67) – (380,189.67) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (330,89.33) – (330,139.67) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (380,89.33) – (380,139.67) ;

(382.36,158.11) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(319.36,158.11) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(334.53,106.94) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi_f( \varphi )$;

(347.61,163.47) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

as in <ref>, then the assignment $a\mapsto \pi_2(C,a)$ and $f\mapsto \Phi_f$ forms a $\pi_2$-opindexing on $(C_0,HC)$.

We first prove that $\Phi_f$ is a morphism of monoids from $\pi_2(C,b)$ to $\pi_2(C,a)$. Let $\varphi,\varphi'\in\pi_2(C,b)$. Consider the composite square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.67,110) – (290.67,110) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.67,160) – (290.67,160) ;

(240.67,110) – (240.67,160) ;

(290.67,110) – (290.67,160) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.67,210) – (290.67,210) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.67,160) – (240.67,210) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (290.67,160) – (290.67,210) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.48,260.18) – (290.48,260.18) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.48,210.18) – (240.48,260.18) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (290.48,210.18) – (290.48,260.18) ;

(293.03,128.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(230.03,128.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(261.28,177.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi $;

(258.28,133.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(261.09,227.48) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi '$;

Consider the unique factorization of the upper square as

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (130.67,131) – (180.67,131) ;

(130.67,81) – (130.67,131) ;

(180.67,81) – (180.67,131) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (130.67,181) – (180.67,181) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (130.67,131) – (130.67,181) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (180.67,131) – (180.67,181) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (130.67,81) – (180.67,81) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.67,130.2) – (290.67,130.2) ;

(240.67,180.2) – (240.67,130.2) ;

(290.67,180.2) – (290.67,130.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.67,80.2) – (290.67,80.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.67,130.2) – (240.67,80.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (290.67,130.2) – (290.67,80.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.67,180.2) – (290.67,180.2) ;

(183.03,99.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(120.03,99.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(151.28,148.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi $;

(148.28,104.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(294.23,148.24) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(229.23,147.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(250.28,100.7) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi _{f}( \varphi )$;

(259.88,150) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(201.63,125.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $=$;

Substituting, we obtain the equality

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (170.17,60) – (220.17,60) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (170.17,110) – (220.17,110) ;

(170.17,60) – (170.17,110) ;

(220.17,60) – (220.17,110) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (170.17,160) – (220.17,160) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (170.17,110) – (170.17,160) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (220.17,110) – (220.17,160) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (169.98,210.18) – (219.98,210.18) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (169.98,160.18) – (169.98,210.18) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (219.98,160.18) – (219.98,210.18) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (280.27,110.8) – (330.27,110.8) ;

(280.27,160.8) – (280.27,110.8) ;

(330.27,160.8) – (330.27,110.8) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (280.27,60.8) – (330.27,60.8) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (280.27,110.8) – (280.27,60.8) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (330.27,110.8) – (330.27,60.8) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (280.27,160.8) – (330.27,160.8) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (279.98,211) – (329.98,211) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (279.98,161) – (279.98,211) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (329.98,161) – (329.98,211) ;

(222.53,78.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(159.53,78.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(190.78,127.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi $;

(187.78,83.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(190.59,177.48) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi '$;

(333.83,128.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(268.83,128.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(289.88,81.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi _{f}( \varphi )$;

(299.48,130.6) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(241.23,125.94) node [anchor=north west][inner sep=0.75pt]  [font=]  $=$;

(300.59,178.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi '$;

Now consider the unique factorization

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (150.67,151) – (200.67,151) ;

(150.67,101) – (150.67,151) ;

(200.67,101) – (200.67,151) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (150.67,201) – (200.67,201) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (150.67,151) – (150.67,201) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (200.67,151) – (200.67,201) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (150.67,101) – (200.67,101) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (260.67,150.2) – (310.67,150.2) ;

(260.67,200.2) – (260.67,150.2) ;

(310.67,200.2) – (310.67,150.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (260.67,100.2) – (310.67,100.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (260.67,150.2) – (260.67,100.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (310.67,150.2) – (310.67,100.2) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (260.67,200.2) – (310.67,200.2) ;

(203.03,119.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(140.03,119.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(171.28,168.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi '$;

(168.28,124.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(314.23,168.24) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(249.23,167.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(270.28,120.7) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi _{f}( \varphi ')$;

(279.88,170) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(221.63,145.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $=$;

substuting above, we obtain

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (190.17,80) – (240.17,80) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (190.17,130) – (240.17,130) ;

(190.17,80) – (190.17,130) ;

(240.17,80) – (240.17,130) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (190.17,180) – (240.17,180) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (190.17,130) – (190.17,180) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (240.17,130) – (240.17,180) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (189.98,230.18) – (239.98,230.18) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (189.98,180.18) – (189.98,230.18) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (239.98,180.18) – (239.98,230.18) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300.27,129.8) – (350.27,129.8) ;

(300.27,180) – (300.27,230) ;

(350.27,180) – (350.27,230) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300.27,79.8) – (350.27,79.8) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300.27,129.8) – (300.27,79.8) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350.27,129.8) – (350.27,79.8) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300.27,180) – (350.27,180) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300.27,230) – (350.27,230) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (299.98,179.8) – (299.98,129.8) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (349.98,179.8) – (349.98,129.8) ;

(242.53,98.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(179.53,98.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(210.78,147.3) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi $;

(207.78,103.8) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(210.59,197.48) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi '$;

(289.83,199.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(354.03,198.24) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(308.68,99.5) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi _{f}( \varphi )$;

(318.28,199.2) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(261.23,145.94) node [anchor=north west][inner sep=0.75pt]  [font=]  $=$;

(309.48,149.9) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi _{f}( \varphi ')$;

The unique factorization of $\varphi'\boxminus\varphi$ along $U_f$ is thus the composite square appearing in the right hand side of the equality above. We conclude that $\Phi_f(\varphi\boxminus\varphi')=\Phi_f(\varphi')\boxminus\Phi_f(\varphi)$. It is easily seen that $\Phi_f(id_b)=id_a$ and thus $\Phi_f:\pi_2(C,b)\to\pi_2(C,a)$ is a monoid morphism for every $f:a\to b$. The fact that the assignmnet $f\mapsto \Phi_f$ is a functor follows from our running assumption that $L\times R$ is split and normal, see <ref>.

Given a regular framed bicategory $C$, we will denote by $\Phi$, the $\pi_2$-opindexing associated to $C$ in Lemma <ref>.

Let $X$ be a topological space. Let $\rho^\square_2(X)$ be homotopy double groupoid with connections of $X$, see [8]. $\rho^\square_2(X)$ is a biregular framed bicategory. The category of objects of $\rho^\square_2(X)$ is the fundamental groupoid $\Pi_1(X)$ of $X$. Let $\Phi:\Pi_1(X)\to\commMon$ be the $\pi_2$-indexing associated to $\rho^\square_2(X)$. Given an object $x$ of $\rho^\square_2(X)$, the commutative monoid $\pi_2(\rho^\square_2(X),x)$ is the second fundamental group $\pi_2(X,x)$. Let $\gamma:x\to y$ be a homotopy equvalence of paths from $x$ to $y$ in $X$. The morphism $\Phi_\gamma:\pi_2(X,y)\to\pi_2(X,x)$ in Lemma <ref> is the morphism $a\mapsto \gamma a\gamma^{-1}$, $a\in \pi_2(X,y)$. Similar computations for the $\pi_2$-opindexing associated to $\Bord,\Rel ^\ast,\Span ^\ast$, etc.

We determine the $\pi_2$-opindexing associated to the regular framed bicategory $\Eq$. Let $C$ be a category. The commutative monoid $\pi_2(\Eq,C)$ is the commutative monoid of natural endomorphisms $\mbox{\textbf{Nat}}(C)$ of $id_C$. The $\pi_2$-indexing $\Phi$ in Lemma <ref> thus associates to every category $C$, the monoid $\mbox{\textbf{Nat}}(C)$. Given an equivalence $F:C\to D$, the morphism $\Phi_F:\mbox{\textbf{Nat}}(D)\to\mbox{\textbf{Nat}}(C)$ associates to every $\nu:id_D\Rightarrow id_D$, the natural transformation provided by the pasting diagram

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
C   D   D   C
[->,font=,>=angle 90]
(m-1-1) edge node [below]$F$ (m-1-2)
(m-1-1) edge [red,bend left=65]node [] (m-1-4)
(m-1-1) edge [white,bend left=35]node [black]$\Downarrow\eta^{-1}$ (m-1-4)
(m-1-1) edge [red,bend right=65]node [] (m-1-4)
(m-1-1) edge [white,bend right=35]node [black]$\Downarrow\eta$ (m-1-4)
(m-1-2) edge [red, bend right=45]node [below] (m-1-3)
(m-1-2) edge [red, bend left=45]node [below] (m-1-3)
(m-1-2) edge [white]node [black]$\Downarrow\nu$ (m-1-3)
(m-1-3) edge node [below]$F^{-1}$ (m-1-4)

where $F^{-1},\eta$ are part of an adjoint equivalence $(F,F^{-1},\eta,\epsilon)$.

The following is the main theorem of this note. Theorem <ref> will be a direct consequence of it.

Let $C$ be a regular framed bicategory. There exists a unique strict double functor

\[q:C_0\rtimes_\Phi HC\to \gamma C\]

such that $H^\ast q=id_{(C_0,HC)}$ and such that $q$ is surjective on squares.

Squares in $HC\rtimes_\Phi C_0$ are either globular squares in $C$ or are of the form $(\varphi_\downarrow, f,\varphi_\uparrow)$ for globular squares $\varphi_\uparrow,\varphi_\downarrow$, and a nontrivial vertical morphism $f$ as in Section <ref>. The condition that $H^\ast q$ should be equal to $id_{(C_0,HC)}$ determines $q$ on objects, arrows, and globular squares of $C$. $q$ is trivially compatible with horizontal and vertical compositions of globular squares. Let $\varphi=(\varphi_\downarrow, f,\varphi_\uparrow)$ be a nonglobular square in $HC\rtimes_\Phi C_0$. Again, the condition that $H^\ast q$ should be equal to $id_{(C_0,HC)}$, together with the condition that $q$ should be a strict double functor, forces $q(\varphi)$ to be the composite square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,69.4) – (350,69.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,119.4) – (350,119.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,69.4) – (300,119.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,69.4) – (350,119.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,119.4) – (300,169.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (350,119.4) – (350,169.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,169.4) – (350,169.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,219) – (350,219) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,169) – (300,219) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,169) – (350,219) ;

(352.36,135.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(289.36,134.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(318.36,185.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow }$;

(318.21,137.5) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(317.96,84.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\uparrow }$;

We must prove that the assignment described above, is compatible with horizontal and vertical identity squares, and compositions. Let $f$ be a nontrivial vertical morphism. The horizontal identity square of $f$ in $C_0\rtimes_\Phi HC$ is the square $(id, f, id)$. $q$ applied to this square is equal to the horizontal identity square $U_f$ of $f$ in $C$. $q$ is thus compatible with horizontal identity squares. Given two horizontally composable squares $\varphi=(\varphi_\downarrow, f,\varphi_\uparrow)$ and $\psi=(\psi_\downarrow, f,\psi_\uparrow)$, the horizontal composition $\varphi\boxvert\psi$ is the square $(\varphi_\downarrow\boxvert \psi_\downarrow, f,\varphi_\uparrow\boxvert\psi_\uparrow)$, where the $\boxvert$ symbol inside the brackets is the horizontal composition of the corresponding globular squares in $HC$. $q(\varphi\boxvert \psi)$ is the horizontal composition

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (320,89.4) – (370,89.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,139.4) – (370,139.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,89.4) – (320,139.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (370,89.4) – (370,139.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (320,139.4) – (320,189.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (370,139.4) – (370,189.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,189.4) – (370,189.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (320,239) – (370,239) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,189) – (320,239) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (370,189) – (370,239) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (370.21,89.47) – (420.21,89.47) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (370.21,139.47) – (420.21,139.47) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (420.21,89.47) – (420.21,139.47) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (420.21,139.47) – (420.21,189.47) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (370.21,189.47) – (420.21,189.47) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (370.21,239.07) – (420.21,239.07) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (420.21,189.07) – (420.21,239.07) ;

(309.36,154.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(338.36,205.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow }$;

(338.21,157.5) node [anchor=north west][inner sep=0.75pt]  [font=]  $U_{f}$;

(337.96,104.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\uparrow }$;

(422.57,155.91) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(388.57,205.51) node [anchor=north west][inner sep=0.75pt]  [font=]  $\psi _{\downarrow }$;

(388.42,157.57) node [anchor=north west][inner sep=0.75pt]  [font=]  $U_{f}$;

(388.17,104.71) node [anchor=north west][inner sep=0.75pt]  [font=]  $\psi _{\uparrow }$;

in $C$. By the exchange relation, this square can be interpreted as the vertical composite of the corresponding three horizontal composite squares above. The middle square is the horizontal identity square $U_f$, and thus the above square is

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (320,89.4) – (370,89.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,139.4) – (370,139.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,89.4) – (320,139.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (370,89.4) – (370,139.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (320,139.4) – (320,189.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (370,139.4) – (370,189.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,189.4) – (370,189.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (320,239) – (370,239) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,189) – (320,239) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (370,189) – (370,239) ;

(372.36,155.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(309.36,154.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(325.36,207.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow } \boxbar \psi _{\downarrow }$;

(338.21,157.5) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(323.96,107.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\uparrow } \boxbar \psi _{\uparrow }$;

The image $q(\varphi\boxvert \psi)$ of $\varphi\boxvert\psi$, under $q$, is thus $q(\varphi)\boxvert q(\psi)$. We conclude that $q$ is compatible with horizontal composition. $q$ is clearly compatible with vertical identities. We now prove compatibility with vertical composition. Let $\varphi=(\varphi_\downarrow, f,\varphi_\uparrow)$ and $\psi=(\psi_\downarrow, g,\psi_\uparrow)$, where $\varphi_\downarrow$ and $\psi_\uparrow$ are vertically composable globular squares in $C$. The vertical composition $\psi\boxminus \varphi$ is the square The vertical composition $\psi\boxminus \varphi$ is the square

\[(\psi_\downarrow\boxminus\Phi_g(\psi_\uparrow\boxminus\varphi_\downarrow), gf, \varphi_\uparrow)\]

The vertical composition $q(\psi)\boxminus q(\psi)$ is, on the other hand, the composite

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,69.4) – (350,69.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,119.4) – (350,119.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,69.4) – (300,119.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,69.4) – (350,119.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,119.4) – (300,169.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (350,119.4) – (350,169.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,169.4) – (350,169.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,219) – (350,219) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,169) – (300,219) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,169) – (350,219) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,268.4) – (350,268.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,218.4) – (300,268.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,218.4) – (350,268.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,268.4) – (300,318.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (350,268.4) – (350,318.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,318.4) – (350,318.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,368) – (350,368) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,318) – (300,368) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,318) – (350,368) ;

(352.36,135.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(289.36,134.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(318.36,185.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow }$;

(318.21,137.5) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(317.96,84.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\uparrow }$;

(352.36,284.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(289.36,283.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(318.36,334.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $\psi _{\downarrow }$;

(318.21,286.5) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(317.96,233.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\psi _{\uparrow }$;

Consider the middle square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (320,91) – (320,141) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (370,91) – (370,141) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,141) – (370,141) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (320,190.6) – (370,190.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,140.6) – (320,190.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (370,140.6) – (370,190.6) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,240) – (370,240) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,190) – (320,240) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (370,190) – (370,240) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (320,91) – (370,91) ;

(372.36,107.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(309.36,106.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(338.36,157.04) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow }$;

(338.21,109.1) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(337.96,205.24) node [anchor=north west][inner sep=0.75pt]  [font=]  $\psi _{\uparrow }$;

This is equal, in $C$, to the square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (340,111) – (340,161) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (390,111) – (390,161) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (340,161) – (390,161) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (340,111) – (390,111) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (340,60.67) – (340,110.67) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (390,60.67) – (390,110.67) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (340,60.67) – (390,60.67) ;

(392.36,127.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(329.36,126.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $g$;

(358.21,129.1) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(340.63,80.57) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi _{g}( \psi _{\uparrow } \boxminus \varphi _{\downarrow })$;

Substituting, the composite $q(\psi)\boxminus q(\psi)$ is equal to the square

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (282.1,201.35) – (332.1,201.35) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (282.1,201.35) – (282.1,251.35) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (332.1,201.35) – (332.1,251.35) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (282,301.4) – (282,351.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (332,301.4) – (332,351.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (282,351.4) – (332,351.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (282,401) – (332,401) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (282,351) – (282,401) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (332,351) – (332,401) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (282.17,301.27) – (332.17,301.27) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (282.17,251.27) – (282.17,301.27) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (332.17,251.27) – (332.17,301.27) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (282.17,251.27) – (332.17,251.27) ;

(300.06,216.59) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\uparrow }$;

(335.36,317.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $gf$;

(266.36,316.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $gf$;

(300.36,367.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $\psi _{\downarrow }$;

(300.21,319.5) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(283.8,271.17) node [anchor=north west][inner sep=0.75pt]  [font=]  $\Phi _{g}( \psi _{\uparrow } \boxminus \varphi _{\downarrow })$;

This is precisely the square $q(\varphi\boxminus\psi)$. The double functor $q$ is thus compatible with vertical composition, and is thus a strict double functor $q:HC\rtimes_\Phi C_0\to \gamma C$. Moreover, $q$ is clearly the unique functor as above, satisfying the equation $H^\ast q=id_{(HC,C_0)}$. Finally, $q$ is clearly surjective on globular squares and horizontal identity squares of $C$. The fact that every square in $\gamma C$ admits a subdivision into globular and horizontal identity squares, implies that $q$ is surjective on squares. This concludes the proof.

With the aid of Theorem <ref> we can now prove Theorem <ref>.

Proof of Theorem <ref>
Let $C$ be a regular framed bicategory. By Theorem <ref> and <cit.> every length 1 globularly generated square admits a canonical form, see <cit.>. The theorem follows directly from this and from <cit.>. $\square$

A natural question is when the double functor $q$ appearing in Theorem <ref> is a double functor, and when it is not. The following is an example of when it is not. The argument rests on the comment appearing as a warning in Section <ref>, where decompositions of squares $(\varphi_\downarrow,f,\varphi_\uparrow)$ is $\crossb$ are unique, while in general regular framed bicategories they are not.

The double functor appearing in the statement of Theorem <ref> is, in general, not a double isomorphism. To see this, consider the double category $\Span ^\ast$. By Proposition <ref>, $\Span ^\ast$ is a regularly framed bicategory. Consider diagrams of the form

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
X   X   X      X   X   X

X   X   X      X   X   X

X   X   X      X   X   X

X   X   X      X   X   X
[->,font=,>=angle 90]
(m-1-2) edge node [above]$\alpha$ (m-1-1)
edge node [above]$\alpha$ (m-1-3)
edge node [left]$\alpha$ (m-2-2)
(m-1-1) edge [red]node (m-2-1)
(m-1-3) edge [red]node (m-2-3)
(m-2-2) edge [red]node [above] (m-2-1)
edge [red]node [left] (m-2-3)
edge node [left]$f$ (m-3-2)
(m-2-1) edge node [left]$f$ (m-3-1)
(m-2-3) edge node [right]$f$ (m-3-3)
(m-3-2) edge [red]node [below] (m-3-1)
edge [red]node [below] (m-3-3)
edge node [left]$\beta$ (m-4-2)
(m-3-1) edge [red]node  (m-4-1)
(m-3-3) edge [red]node  (m-4-3)
(m-4-2) edge node [below]$\gamma$ (m-4-1)
edge node [below]$\gamma$ (m-4-3)

(m-1-6) edge node [above]$\alpha$ (m-1-5)
edge node [above]$\alpha$ (m-1-7)
edge node [left]$\alpha$ (m-2-6)
(m-1-5) edge [red]node [](m-2-5)
(m-1-7) edge [red]node [](m-2-7)
(m-2-6) edge [red]node  (m-2-5)
edge [red]node [right] (m-2-7)
edge node [left]$f$ (m-3-6)
(m-2-5) edge node [left]$f$ (m-3-5)
(m-2-7) edge node [right]$f$ (m-3-7)
(m-3-6) edge [red]node  (m-3-5)
edge [red]node  (m-3-7)
(m-3-5) edge[red] node[left] (m-4-5)
(m-3-6) edge node[left]$\beta'$ (m-4-6)
(m-3-7) edge[red] node[left] (m-4-7)
(m-4-6) edge node[below]$\gamma$ (m-4-5)
edge node[below]$\gamma$ (m-4-7)

where $X$ is an infinite set, $f;X\to X$ is a bijection such that $f\neq id_X$, $\gamma:X\to X$ is a surjective function that is not bijective, $\beta,\beta'$ are right inverses of $\gamma$ such that $\beta\neq\beta'$,  and such that $\beta f\alpha=\beta' f\alpha$, then if we write $\overline{\alpha}$ for the top diagram in the above two squares, and $\underline{\beta},\underline{\beta'}$ for the bottom diagrams above, then the squares $\psi=(\underline{\beta}, f, \overline{\alpha})$ and $\psi'=(\underline{\beta'}, f, \overline{\alpha})$ are different in $H\Span ^\ast\rtimes_\Phi \Set^\ast$, but the images $q(\psi)$ and $q(\psi')$ under the double functor $q$ o Theorem <ref> are both equal to the square

(m)[matrix of math nodes, row sep=2em, column sep=2em,text height=1.5ex, text depth=0.25ex]
X   X   X

X   X   X
[->,font=,>=angle 90]
(m-1-2) edge node [above]$\alpha$ (m-1-1)
edge node [above]$\alpha$ (m-1-3)
edge node [left]$\eta$ (m-2-2)
(m-1-1) edge node [left]$f$(m-2-1)
(m-1-3) edge node [right]$f$(m-2-3)
(m-2-2) edge node [below]$\gamma$ (m-2-1)
edge node [below]$\gamma$ (m-2-3)

in $\Span ^\ast$, where $\beta f\alpha=\beta' f\alpha$. We conclude that in this case $q$ is not bijective on squares.

The following Observation provides conditions for the double functor $q$ to be a bijection.

Let $C$ be a regular framed bicategory. If $C$ is a double groupoid, then the double functor $q$ appearing in Theorem <ref> is a double isomorphism. This follows directly from the fact that for nonglobular squares of the form

every picture/.style=line width=0.75pt

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,69.4) – (350,69.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,119.4) – (350,119.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,69.4) – (300,119.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,69.4) – (350,119.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,119.4) – (300,169.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (350,119.4) – (350,169.4) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,169.4) – (350,169.4) ;

[color=rgb, 255:red, 0; green, 0; blue, 0   ,draw opacity=1 ]   (300,219) – (350,219) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (300,169) – (300,219) ;

[color=rgb, 255:red, 208; green, 2; blue, 27   ,draw opacity=1 ]   (350,169) – (350,219) ;

(352.36,135.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(289.36,134.84) node [anchor=north west][inner sep=0.75pt]  [font=]  $f$;

(318.36,185.44) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\downarrow }$;

(318.21,137.5) node [anchor=north west][inner sep=0.75pt]  [font=]  $U$;

(317.96,84.64) node [anchor=north west][inner sep=0.75pt]  [font=]  $\varphi _{\uparrow }$;

in a double groupoid $C$ admit a unique such decomposition.

PROBLEMA: En general en la categoria doble C no sabemos si existen cuadrados con la frontera como la queremos, o sea con f,f id abajo y dos betas arriba. En general no podemos garantizar la existencia de cuadrados de ninguna forma excepto de la forma del producto cruzado.

Let $\boxdot\Set$ be the double category of commuting squares on $\Set$. The horizontal 2-category $H\boxdot\Set$ of $\boxdot\Set$ is the trivial 2-category on $\Set$, i.e. the 2-category whose underlying category is $\Set$ and whose 2-cells are all identities. In square notation, the 2-cells in $H\boxdot\Set$ are the squares of the form

\[Squares\]

Given a set $X$, the commutative monoid $\pi_2(\boxdot \Set,X)$ has a single element, namely the square

\[Trivial square\]

thus $\pi_2(\boxdot \Set,X)$ is the zero commutative monoid 0. Let $\Phi:\Set\to\commMon$ be the constant functor on 0. Thus defined $\Phi$ is a $\pi_2$-indexing on $(H\boxdot\Set,\Set)$. The double category $H\boxdot\Set\rtimes_\Phi\Set$ is the double category whose only squares are commuting squares of the form:

\[Two squares\]

We claim that there does not exist a framed bicategory $C$ (regular, opregular, or neither) such that there exists a strict double functor $q:H\boxdot\Set\rtimes_\Phi\Set\to\gamma C$ satisfying the conditions in the statement of Theorem <ref>. Suppose there exists one such $q$. Let $X$ be a set, and $f:X\to X$ be a function such that $f\neq id$. Consider the niche

\[Niche\]

The horizontal identity

\[Identity\]

is the unique filler of the above niche in $H\boxdot\Set\rtimes_\Phi\Set$. To see this observe that if $\varphi=|\varphi_\downarrow\rangle f\langle \varphi_\uparrow|$ is a filler square, then $\varphi_\downarrow$ and $\varphi_\uparrow$ must be 2-cells in $\boxdot \Set$, and thus must be identities. We conclude that $|id\rangle f\langle id|$ is the unique filler of the above niche in $H\boxdot\Set\rtimes_\Phi\Set$. Consider now the same niche in $C$, and consider its opCartesian filler

\[opCartesian\]

From the condition that $q$ should be surjective on squares, and the identity on boundaries of squares, it follows that the above square is the image of a filler of the same niche in $H\boxdot\Set\rtimes_\Phi\Set$, and thus it is of the form

\[identity bottom too\]

Choose a set $X$, and a function $f:X\to X$ now, such that there exists another function $\alpha:X\to X$ such that $\alpha\neq id$ and such that $\alpha f=f$. The square

\[alpha bottom\]

is a square in

[1]
R. Gordon, A. J. Power, and R. Street.
Coherence for tricategories.
Memoirs of the American Mathematical Society, 117(558), 1999.

[2]
M. A. Shulman.
Framed bicategories and monoidal fibrations.
Theory and Applications Categories, 18:650–738, 2008.

[3]
M. A. Shulman.
Comparing composites of left and right derived functors.
New York Journal of Mathematics, 17:75–125, 2011.

[4]
J. Orendain.
Lifting bicategories into double categories: The globularily generated condition.
Theory and Applications of Categories, 34:80–108, 2019.

[5]
J. Orendain.
Free globularly generated double categories.
Cahiers de topologie et géometrie différentielle catégoriques, LXII Issue 3:243–302, 2021.

[6]
J. Orendain.
Free globularly generated double categories ii: The canonical double projection.
Theory and Applications of Categories, 34(42):1343–1385, 2019.

[7]
J. Orendain and R. Maldonado-Herrera.
Internalizations of decorated bicategories via $\pi_2$-indexings.
arXiv:2310.18673, 2023.

[8]
R. Brown and G. H. Mosa.
Double categories, 2-categories, thin structures and connections.
Theory Appl. Categ., 5(7):163–1757, 1999.