Definitions for Framed bicategories and monoidal fibrations

QAlgorithms.Papers.Independent.Intakethird100.P60.Companion

For arbitrary universe levels $u,v,w,x$, a category $V$ with objects in universe $u$ and morphisms in universe $v$, and data $D$ supplying horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, horizontal units $I_A$, horizontal products $*$, identity squares $1_M$, vertical composition $;$, horizontal composition $\Box$, unit squares $U_f\in\operatorname{Sq}(f,f;I_A,I_B)$, and associativity and unit comparison squares in both directions, fix any objects $A,B$, morphism $f:A\to B$, and $M\in H(A,B)$. This structure consists of a square $\varepsilon\in\operatorname{Sq}(f,1_B;M,I_B)$, a square $\eta\in\operatorname{Sq}(1_A,f;I_A,M)$, a heterogeneous equality between the vertical composite $\eta;\varepsilon$ and $U_f$, and the equation

$$\bigl(\bar\lambda_M;(\eta\mathbin{\Box}\varepsilon)\bigr);\rho_M=1_M.$$

Here $\bar\lambda_M\in\operatorname{Sq}(1_A,1_B;M,I_A*M)$ and $\rho_M\in\operatorname{Sq}(1_A,1_B;M*I_B,M)$ are the supplied comparison squares; $\eta\mathbin{\Box}\varepsilon$ is the supplied horizontal composite from $I_A*M$ to $M*I_B$ with identity side morphisms. Each semicolon means composition in the displayed order; in the displayed equation, the composites of identity side morphisms are simplified to identities. Heterogeneous equality allows the vertical equation to compare terms whose displayed dependent types are not definitionally identical. No other coherence equations for $D$ are assumed, and the objects $A,B$ may coincide; defining this structure does not assert that it is inhabited for every $f,M$.

QAlgorithms.Papers.Independent.Intakethird100.P60.Conjoint

For arbitrary universe levels $u,v,w,x$, a category $V$ with objects in universe $u$ and morphisms in universe $v$, and data $D$ supplying horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, horizontal units $I_A$, horizontal products $*$, identity squares $1_M$, vertical composition $;$, horizontal composition $\Box$, unit squares $U_f\in\operatorname{Sq}(f,f;I_A,I_B)$, and associativity and unit comparison squares in both directions, fix any objects $A,B$, morphism $f:A\to B$, and $N\in H(B,A)$. This structure consists of a square $\varepsilon\in\operatorname{Sq}(1_B,f;N,I_B)$, a square $\eta\in\operatorname{Sq}(f,1_A;I_A,N)$, a heterogeneous equality between the vertical composite $\eta;\varepsilon$ and $U_f$, and the equation

$$\bigl(\bar\rho_N;(\varepsilon\mathbin{\Box}\eta)\bigr);\lambda_N=1_N.$$

Here $\bar\rho_N\in\operatorname{Sq}(1_B,1_A;N,N*I_A)$ and $\lambda_N\in\operatorname{Sq}(1_B,1_A;I_B*N,N)$ are the supplied comparison squares; $\varepsilon\mathbin{\Box}\eta$ is the supplied horizontal composite from $N*I_A$ to $I_B*N$ with identity side morphisms. Each semicolon means composition in the displayed order; in the displayed equation, the composites of identity side morphisms are simplified to identities. Heterogeneous equality allows the vertical equation to compare terms whose displayed dependent types are not definitionally identical. No other coherence equations for $D$ are assumed, and the objects $A,B$ may coincide; defining this structure does not assert that it is inhabited for every $f,N$.

QAlgorithms.Papers.Independent.Intakethird100.P60.DoubleCoherence

For arbitrary universe levels $u,v,w,x$, let $V$ be a category with objects in universe $u$ and morphisms in universe $v$, and let $D$ supply horizontal-arrow types $H(A,B)$ in universe $w$ and square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, where $f:A\to C$, $g:B\to E$, $M\in H(A,B)$, and $N\in H(C,E)$. Write $I_A\in H(A,A)$ for the supplied horizontal unit, $M*N$ for the supplied horizontal product, $1_M$ for its identity square, $a;b$ for vertical composition in the order $a$ then $b$, $a\mathbin{\Box}b$ for horizontal composition, and $U_f\in\operatorname{Sq}(f,f;I_A,I_B)$ for the supplied square associated to $f:A\to B$. Write $\alpha_{M,N,P}:(M*N)*P\to M*(N*P)$ and $\bar\alpha_{M,N,P}$ for the supplied comparison in the reverse direction, and write $\lambda_M:I_A*M\to M$, $\bar\lambda_M:M\to I_A*M$, $\rho_M:M*I_B\to M$, and $\bar\rho_M:M\to M*I_B$; these comparison arrows are squares with identity side morphisms. In equations involving only identity-side squares, $;$ means vertical composition with the identity side composites simplified. Let $\doteq$ denote heterogeneous equality, which allows equality to be expressed when the displayed dependent types are not definitionally identical; ordinary $=$ denotes equality within the same type. This proposition consists of all the following universally quantified equations. For every eight objects $A,B,C,E,F,G,I,J$, morphisms $f:A\to C$, $g:B\to E$, $h:C\to F$, $k:E\to G$, $l:F\to I$, $m:G\to J$, horizontal elements $M\in H(A,B)$, $N\in H(C,E)$, $P\in H(F,G)$, $Q\in H(I,J)$, and squares $a\in\operatorname{Sq}(f,g;M,N)$, $b\in\operatorname{Sq}(h,k;N,P)$, $c\in\operatorname{Sq}(l,m;P,Q)$, one has $(a;b);c\doteq a;(b;c)$. For every four objects $A,B,C,E$, morphisms $f:A\to C$, $g:B\to E$, elements $M\in H(A,B)$, $N\in H(C,E)$, and square $a\in\operatorname{Sq}(f,g;M,N)$, one has $1_M;a\doteq a$ and $a;1_N\doteq a$. For every object $A$, $U_{1_A}=1_{I_A}$; for every three objects $A,B,C$ and morphisms $f:A\to B$, $g:B\to C$, $U_{g\circ f}=U_f;U_g$; and for every $M\in H(A,B)$, $N\in H(B,C)$, $1_M\mathbin{\Box}1_N=1_{M*N}$. For every nine objects $A,B,C,E,F,G,I,J,K$, morphisms $f:A\to E$, $g:B\to F$, $h:C\to G$, $i:E\to I$, $j:F\to J$, $k:G\to K$, horizontal elements $M\in H(A,B)$, $N\in H(B,C)$, $P\in H(E,F)$, $Q\in H(F,G)$, $R\in H(I,J)$, $S\in H(J,K)$, and squares $a\in\operatorname{Sq}(f,g;M,P)$, $b\in\operatorname{Sq}(g,h;N,Q)$, $c\in\operatorname{Sq}(i,j;P,R)$, $d\in\operatorname{Sq}(j,k;Q,S)$, one has

$$(a\mathbin{\Box}b);(c\mathbin{\Box}d)=(a;c)\mathbin{\Box}(b;d).$$

For every four objects $A,B,C,E$ and $M\in H(A,B)$, $N\in H(B,C)$, $P\in H(C,E)$, both equations

$$\alpha_{M,N,P};\bar\alpha_{M,N,P}=1_{(M*N)*P}, \qquad \bar\alpha_{M,N,P};\alpha_{M,N,P}=1_{M*(N*P)}$$

hold. For every pair of objects $A,B$ and $M\in H(A,B)$, all four equations

$$\lambda_M;\bar\lambda_M=1_{I_A*M},\qquad \bar\lambda_M;\lambda_M=1_M,\qquad \rho_M;\bar\rho_M=1_{M*I_B},\qquad \bar\rho_M;\rho_M=1_M$$

hold. For every eight objects $A,B,C,E,F,G,I,J$, morphisms $f:A\to F$, $g:B\to G$, $h:C\to I$, $k:E\to J$, elements $M\in H(A,B)$, $N\in H(B,C)$, $P\in H(C,E)$, $Q\in H(F,G)$, $R\in H(G,I)$, $S\in H(I,J)$, and squares $a\in\operatorname{Sq}(f,g;M,Q)$, $b\in\operatorname{Sq}(g,h;N,R)$, $c\in\operatorname{Sq}(h,k;P,S)$, one has

$$((a\mathbin{\Box}b)\mathbin{\Box}c);\alpha_{Q,R,S} \doteq \alpha_{M,N,P};(a\mathbin{\Box}(b\mathbin{\Box}c)).$$

For every four objects $A,B,C,E$, morphisms $f:A\to C$, $g:B\to E$, elements $M\in H(A,B)$, $N\in H(C,E)$, and square $a\in\operatorname{Sq}(f,g;M,N)$, one has

$$(U_f\mathbin{\Box}a);\lambda_N\doteq\lambda_M;a, \qquad (a\mathbin{\Box}U_g);\rho_N\doteq\rho_M;a.$$

For every five objects $A,B,C,E,F$ and $M\in H(A,B)$, $N\in H(B,C)$, $P\in H(C,E)$, $Q\in H(E,F)$, one has

$$\bigl((\alpha_{M,N,P}\mathbin{\Box}1_Q);\alpha_{M,N*P,Q}\bigr); (1_M\mathbin{\Box}\alpha_{N,P,Q}) = \alpha_{M*N,P,Q};\alpha_{M,N,P*Q}.$$

Finally, for every three objects $A,B,C$ and $M\in H(A,B)$, $N\in H(B,C)$, one has

$$\alpha_{M,I_B,N};(1_M\mathbin{\Box}\lambda_N) = \rho_M\mathbin{\Box}1_N.$$

All object choices may include repetitions; each requirement ranges over every inhabitant of the specified types, and a universally quantified requirement has no instances when one of its required input types is empty.

QAlgorithms.Papers.Independent.Intakethird100.P60.DoubleData

For any universe levels $u,v,w,x$ and any type $V$ in universe $u$ equipped with a category structure whose morphism types lie in universe $v$, this structure consists of the following data. For every pair of objects $A,B$, there is a type $H(A,B)$ in universe $w$; for every four objects $A,B,C,D$, morphisms $f:A\to C$, $g:B\to D$, and elements $M\in H(A,B)$, $N\in H(C,D)$, there is a type of squares $\operatorname{Sq}(f,g;M,N)$ in universe $x$. There are chosen elements $I_A\in H(A,A)$ for every object $A$, and products $M*N\in H(A,C)$ for every $M\in H(A,B)$, $N\in H(B,C)$. Every $M\in H(A,B)$ has a chosen identity square $1_M\in\operatorname{Sq}(1_A,1_B;M,M)$. For arbitrary objects $A,B,C,D,E,F$, morphisms $f:A\to C$, $g:B\to D$, $h:C\to E$, $k:D\to F$, horizontal elements $M\in H(A,B)$, $N\in H(C,D)$, $P\in H(E,F)$, and squares $a\in\operatorname{Sq}(f,g;M,N)$, $b\in\operatorname{Sq}(h,k;N,P)$, there is a specified vertical composite $a;b\in\operatorname{Sq}(h\circ f,k\circ g;M,P)$. Every morphism $f:A\to B$ has a specified square $U_f\in\operatorname{Sq}(f,f;I_A,I_B)$. For arbitrary objects $A,B,C,D,E,F$, morphisms $f:A\to D$, $g:B\to E$, $h:C\to F$, horizontal elements $M\in H(A,B)$, $N\in H(B,C)$, $P\in H(D,E)$, $Q\in H(E,F)$, and squares $a\in\operatorname{Sq}(f,g;M,P)$, $b\in\operatorname{Sq}(g,h;N,Q)$, there is a specified horizontal composite $a\mathbin{\Box}b\in\operatorname{Sq}(f,h;M*N,P*Q)$. For every composable triple $M\in H(A,B)$, $N\in H(B,C)$, $P\in H(C,D)$, there are specified squares $\alpha_{M,N,P}\in\operatorname{Sq}(1_A,1_D;(M*N)*P,M*(N*P))$ and $\bar\alpha_{M,N,P}\in\operatorname{Sq}(1_A,1_D;M*(N*P),(M*N)*P)$. For every $M\in H(A,B)$, there are specified squares $\lambda_M:I_A*M\to M$, $\bar\lambda_M:M\to I_A*M$, $\rho_M:M*I_B\to M$, and $\bar\rho_M:M\to M*I_B$, where each arrow here denotes a square with side morphisms $1_A,1_B$. This structure imposes no equations on these operations; in particular, the oppositely directed comparison squares are supplied without equations asserting that they are inverses. Objects may coincide, and no nonemptiness of $V$ or of arbitrary horizontal-arrow or square types is separately assumed.

QAlgorithms.Papers.Independent.Intakethird100.P60.DoubleData.seq

For arbitrary universe levels $u,v,w,x$, a category $V$ with object type in universe $u$ and morphism types in universe $v$, and supplied data $D$ consisting of horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, and the specified units, products, identity squares, compositions, and comparison squares, this definition provides the following operation. For every pair of objects $A,B$, every $M,N,P\in H(A,B)$, and squares $a\in\operatorname{Sq}(1_A,1_B;M,N)$, $b\in\operatorname{Sq}(1_A,1_B;N,P)$, it returns a square in $\operatorname{Sq}(1_A,1_B;M,P)$: specifically, it is the supplied vertical composite of $a$ followed by $b$, whose side morphisms $1_A\circ1_A$ and $1_B\circ1_B$ are identified with $1_A$ and $1_B$ using the category identity laws. Here a square type records its two side morphisms and its source and target horizontal elements; vertical composition composes both side morphisms and joins squares with a common horizontal boundary. The definition assumes no coherence equations for $D$, permits coinciding objects or horizontal elements, and requires inputs only when the indicated types are inhabited.

QAlgorithms.Papers.Independent.Intakethird100.P60.HasCompanions

For arbitrary universe levels $u,v,w,x$, a category $V$ with objects in universe $u$ and morphisms in universe $v$, and data $D$ supplying horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, horizontal units $I_A$, products $*$, identity squares $1_M$, vertical composition $;$, horizontal composition $\Box$, unit squares $U_f\in\operatorname{Sq}(f,f;I_A,I_B)$, and associativity and unit comparison squares in both directions, this property says that for every pair of objects $A,B$ and every morphism $f:A\to B$, there exist $M\in H(A,B)$ and squares $\varepsilon\in\operatorname{Sq}(f,1_B;M,I_B)$, $\eta\in\operatorname{Sq}(1_A,f;I_A,M)$ such that $\eta;\varepsilon$ is heterogeneously equal to $U_f$ and

$$\bigl(\bar\lambda_M;(\eta\mathbin{\Box}\varepsilon)\bigr);\rho_M=1_M.$$

Here $\bar\lambda_M$ is the supplied identity-side square $M\to I_A*M$, $\rho_M$ is the supplied identity-side square $M*I_B\to M$, and the displayed semicolons denote vertical composition in the indicated order with identity side composites simplified. Heterogeneous equality allows comparison of terms whose displayed dependent types are not definitionally identical. The claim is existence of such data and proofs, with no uniqueness requirement and no simultaneous choice specified. No coherence equations for $D$ are assumed. The objects may coincide; a pair with no morphisms imposes no requirement, and the whole property is vacuous if $V$ has no objects.

QAlgorithms.Papers.Independent.Intakethird100.P60.HasConjoints

For arbitrary universe levels $u,v,w,x$, a category $V$ with objects in universe $u$ and morphisms in universe $v$, and data $D$ supplying horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, horizontal units $I_A$, products $*$, identity squares $1_M$, vertical composition $;$, horizontal composition $\Box$, unit squares $U_f\in\operatorname{Sq}(f,f;I_A,I_B)$, and associativity and unit comparison squares in both directions, this property says that for every pair of objects $A,B$ and every morphism $f:A\to B$, there exist $N\in H(B,A)$ and squares $\varepsilon\in\operatorname{Sq}(1_B,f;N,I_B)$, $\eta\in\operatorname{Sq}(f,1_A;I_A,N)$ such that $\eta;\varepsilon$ is heterogeneously equal to $U_f$ and

$$\bigl(\bar\rho_N;(\varepsilon\mathbin{\Box}\eta)\bigr);\lambda_N=1_N.$$

Here $\bar\rho_N$ is the supplied identity-side square $N\to N*I_A$, $\lambda_N$ is the supplied identity-side square $I_B*N\to N$, and the displayed semicolons denote vertical composition in the indicated order with identity side composites simplified. Heterogeneous equality allows comparison of terms whose displayed dependent types are not definitionally identical. The claim is existence of such data and proofs, with no uniqueness requirement and no simultaneous choice specified. No coherence equations for $D$ are assumed. The objects may coincide; a pair with no morphisms imposes no requirement, and the whole property is vacuous if $V$ has no objects.

QAlgorithms.Papers.Independent.Intakethird100.P60.IsCartesian

For arbitrary universe levels $u,v,w,x$, a category $V$ with objects in universe $u$ and morphisms in universe $v$, and data $D$ supplying horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, and the specified units, products, identity squares, compositions, and comparison squares, fix objects $A,B,C,E$, morphisms $f:A\to C$, $g:B\to E$, horizontal elements $M\in H(A,B)$, $N\in H(C,E)$, and a square $a\in\operatorname{Sq}(f,g;M,N)$. The defined property says that for every pair of objects $P,Q$, morphisms $h:P\to A$, $k:Q\to B$, horizontal element $T\in H(P,Q)$, and square $b\in\operatorname{Sq}(f\circ h,g\circ k;T,N)$, there is exactly one square $c\in\operatorname{Sq}(h,k;T,M)$ such that the supplied vertical composite of $c$ followed by $a$ equals $b$. Thus uniqueness concerns the squares satisfying that equation: any other such square equals $c$. No coherence equations for $D$ are assumed. The object choices may coincide, and choices of $P,Q,h,k,T$ for which the indicated type of $b$ is empty impose no factorization requirement.

QAlgorithms.Papers.Independent.Intakethird100.P60.IsDualPair

Let $V$ be any category and $D$ any of the specified double data, with arbitrary universe sizes. Write $H(A,B)$ for its horizontal-arrow types, $C_{f,g}(M,N)$ for its squares with left and right vertical boundaries $f,g$, $U_A$ for its horizontal units, $MN$ for horizontal multiplication, $1_M$ for identity squares, and $s\otimes t$ for horizontal square composition. For squares with identity vertical boundaries, write $s;t$ for vertical composition in that order, simplifying composites of identity morphisms. The specified associativity squares are $\alpha_{M,N,P}:(MN)P\to M(NP)$ and $\bar\alpha_{M,N,P}:M(NP)\to(MN)P$; the specified unit squares are $\lambda_M:U_AM\to M$, $\bar\lambda_M:M\to U_AM$, $\rho_M:MU_B\to M$, and $\bar\rho_M:M\to MU_B$ for $M\in H(A,B)$, all with identity vertical boundaries. For any objects $A,B$, horizontal arrows $M\in H(A,B)$, $N\in H(B,A)$, and supplied squares

$$\eta\in C_{1_A,1_A}(U_A,MN), \qquad \varepsilon\in C_{1_B,1_B}(NM,U_B),$$

the assertion that these form a dual pair is defined to be exactly the conjunction

$$\begin{aligned} \Bigl(\Bigl(\bigl(\bar\lambda_M;(\eta\otimes1_M)\bigr); \alpha_{M,N,M}\Bigr);(1_M\otimes\varepsilon)\Bigr);\rho_M &=1_M,\\ \Bigl(\Bigl(\bigl(\bar\rho_N;(1_N\otimes\eta)\bigr); \bar\alpha_{N,M,N}\Bigr);(\varepsilon\otimes1_N)\Bigr);\lambda_N &=1_N. \end{aligned}$$

This is a predicate on the supplied $\eta,\varepsilon$; it does not quantify their existence. No coherence assumption on $D$, or distinctness assumption on $A,B$, is imposed.

QAlgorithms.Papers.Independent.Intakethird100.P60.IsFrameFibration

For arbitrary universe levels $u,v,w,x$, a category $V$ with objects in universe $u$ and morphisms in universe $v$, and data $D$ supplying horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, and the specified units, products, identity squares, compositions, and comparison squares, this property means that for every four objects $A,B,C,E$, morphisms $f:A\to C$, $g:B\to E$, and horizontal element $N\in H(C,E)$, there exist a horizontal element $M\in H(A,B)$ and a square $a\in\operatorname{Sq}(f,g;M,N)$ with the following property: for every pair of objects $P,Q$, morphisms $h:P\to A$, $k:Q\to B$, horizontal element $T\in H(P,Q)$, and square $b\in\operatorname{Sq}(f\circ h,g\circ k;T,N)$, there is exactly one $c\in\operatorname{Sq}(h,k;T,M)$ whose supplied vertical composite with $a$, in the order $c$ then $a$, equals $b$. The existentially chosen pair $M,a$ is not required to be unique. No coherence equations for $D$ are assumed. All object choices may coincide; empty types among the universally quantified inputs contribute no instances, so the property holds vacuously when $V$ has no objects, and an empty type of test squares $b$ imposes no factorization requirement for that test.

QAlgorithms.Papers.Independent.Intakethird100.P60.IsFrameOpfibration

For arbitrary universe levels $u,v,w,x$, a category $V$ with objects in universe $u$ and morphisms in universe $v$, and data $D$ supplying horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, and the specified units, products, identity squares, compositions, and comparison squares, this property means that for every four objects $A,B,C,E$, morphisms $f:A\to C$, $g:B\to E$, and horizontal element $M\in H(A,B)$, there exist a horizontal element $N\in H(C,E)$ and a square $a\in\operatorname{Sq}(f,g;M,N)$ with the following property: for every pair of objects $P,Q$, morphisms $h:C\to P$, $k:E\to Q$, horizontal element $T\in H(P,Q)$, and square $b\in\operatorname{Sq}(h\circ f,k\circ g;M,T)$, there is exactly one $c\in\operatorname{Sq}(h,k;N,T)$ whose supplied vertical composite with $a$, in the order $a$ then $c$, equals $b$. The existentially chosen pair $N,a$ is not required to be unique. No coherence equations for $D$ are assumed. All object choices may coincide; empty types among the universally quantified inputs contribute no instances, so the property holds vacuously when $V$ has no objects, and an empty type of test squares $b$ imposes no factorization requirement for that test.

QAlgorithms.Papers.Independent.Intakethird100.P60.IsFramed

For arbitrary universe levels $u,v,w,x$, a category $V$ with objects in universe $u$ and morphisms in universe $v$, and data $D$ supplying horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, and the specified units, products, identity squares, compositions, and comparison squares, this property is defined to mean that for every four objects $A,B,C,E$, morphisms $f:A\to C$, $g:B\to E$, and horizontal element $N\in H(C,E)$, there exist $M\in H(A,B)$ and $a\in\operatorname{Sq}(f,g;M,N)$ such that, for every pair of objects $P,Q$, morphisms $h:P\to A$, $k:Q\to B$, horizontal element $T\in H(P,Q)$, and square $b\in\operatorname{Sq}(f\circ h,g\circ k;T,N)$, there exists exactly one square $c\in\operatorname{Sq}(h,k;T,M)$ whose supplied vertical composite with $a$, in the order $c$ then $a$, equals $b$. The chosen pair $M,a$ need not be unique. No coherence equations for $D$ are included as hypotheses or additional requirements. Objects may coincide, empty universally quantified input types contribute no instances, and the property is vacuous when $V$ has no objects; for any fixed test inputs, an empty type of squares $b$ imposes no factorization requirement.

QAlgorithms.Papers.Independent.Intakethird100.P60.IsOpcartesian

For arbitrary universe levels $u,v,w,x$, a category $V$ with objects in universe $u$ and morphisms in universe $v$, and data $D$ supplying horizontal-arrow types $H(A,B)$ in universe $w$, square types $\operatorname{Sq}(f,g;M,N)$ in universe $x$, and the specified units, products, identity squares, compositions, and comparison squares, fix objects $A,B,C,E$, morphisms $f:A\to C$, $g:B\to E$, horizontal elements $M\in H(A,B)$, $N\in H(C,E)$, and a square $a\in\operatorname{Sq}(f,g;M,N)$. The defined property says that for every pair of objects $P,Q$, morphisms $h:C\to P$, $k:E\to Q$, horizontal element $T\in H(P,Q)$, and square $b\in\operatorname{Sq}(h\circ f,k\circ g;M,T)$, there is exactly one square $c\in\operatorname{Sq}(h,k;N,T)$ such that the supplied vertical composite of $a$ followed by $c$ equals $b$. Thus uniqueness concerns the squares satisfying that equation: any other such square equals $c$. No coherence equations for $D$ are assumed. The object choices may coincide, and choices of $P,Q,h,k,T$ for which the indicated type of $b$ is empty impose no factorization requirement.

QAlgorithms.Papers.Independent.Intakethird100.P60.PseudoConnectionPair

Let $V$ be any category and $D$ any of the specified double data, with arbitrary universe sizes for objects, morphisms, horizontal arrows, and squares. Write $H(A,B)$ for its horizontal-arrow type and $C_{f,g}(M,N)$ for its square type, where $M\in H(A,B)$, $N\in H(C,E)$, $f:A\to C$, and $g:B\to E$. Write $U_A$ for the chosen horizontal unit, $MN$ for horizontal multiplication, $1_M$ for the chosen identity square, $U_f$ for the chosen square from $U_A$ to $U_B$ with both vertical boundaries $f:A\to B$, $s;t$ for vertical composition in that order, and $s\otimes t$ for horizontal composition. For squares with identity vertical boundaries, $s;t$ includes simplifying composites of identity morphisms. Write $\lambda_M:U_AM\to M$, $\bar\lambda_M:M\to U_AM$, and $\rho_M:MU_B\to M$ for the specified unit squares, all with identity vertical boundaries; write $\doteq$ for heterogeneous equality, which permits the compared cells to have differently presented boundary types. A pseudo-connection pair consists of an assignment, for every pair of objects $A,B$ and every morphism $f:A\to B$, of a horizontal arrow $F_f\in H(A,B)$, together with chosen squares

$$u_f\in C_{1_A,f}(U_A,F_f), \qquad e_f\in C_{f,1_B}(F_f,U_B)$$

and proofs of

$$u_f;e_f\doteq U_f, \qquad \bigl(\bar\lambda_{F_f};(u_f\otimes e_f)\bigr);\rho_{F_f}=1_{F_f}.$$

These choices are required for every morphism, including identities. No coherence assumption on $D$ is part of this structure. If $V$ has no objects, the requirements indexed by objects and morphisms are vacuous.

QAlgorithms.Papers.Independent.Intakethird100.P60.PseudoOpConnectionPair

Let $V$ be any category and $D$ any of the specified double data, with arbitrary universe sizes for objects, morphisms, horizontal arrows, and squares. Write $H(A,B)$ for its horizontal-arrow type and $C_{f,g}(M,N)$ for its square type, where $M\in H(A,B)$, $N\in H(C,E)$, $f:A\to C$, and $g:B\to E$. Write $U_A$ for the chosen horizontal unit, $MN$ for horizontal multiplication, $1_M$ for the chosen identity square, $U_f$ for the chosen square from $U_A$ to $U_B$ with both vertical boundaries $f:A\to B$, $s;t$ for vertical composition in that order, and $s\otimes t$ for horizontal composition. For squares with identity vertical boundaries, $s;t$ includes simplifying composites of identity morphisms. Write $\bar\rho_N:N\to NU_A$ and $\lambda_N:U_BN\to N$ for the specified unit squares when $N\in H(B,A)$; their vertical boundaries are identities. Write $\doteq$ for heterogeneous equality, allowing differently presented boundary types. A pseudo-op-connection pair consists of an assignment, for every pair of objects $A,B$ and every morphism $f:A\to B$, of a horizontal arrow $G_f\in H(B,A)$, together with chosen squares

$$u_f\in C_{f,1_A}(U_A,G_f), \qquad e_f\in C_{1_B,f}(G_f,U_B)$$

and proofs of

$$u_f;e_f\doteq U_f, \qquad \bigl(\bar\rho_{G_f};(e_f\otimes u_f)\bigr);\lambda_{G_f}=1_{G_f}.$$

These choices are required for every morphism, including identities. No coherence assumption on $D$ is part of this structure. If $V$ has no objects, the requirements indexed by objects and morphisms are vacuous.

QAlgorithms.Papers.Independent.Intakethird100.P60.baseCoevaluation

Let $V$ be any category and $D$ any of the specified double data, with arbitrary universe sizes. Write $H(A,B)$ for its horizontal-arrow types, $C_{f,g}(M,N)$ for squares with vertical boundaries $f,g$, $U_A$ for horizontal units, $MN$ for horizontal multiplication, $1_M$ for identity squares, $U_f$ for the chosen square on horizontal units with both vertical boundaries $f$, and $\otimes$ for horizontal square composition. Write $s;t$ for vertical composition in that order, with identity boundary composites simplified when appropriate, and $\doteq$ for heterogeneous equality. The specified unit squares are $\lambda_M:U_AM\to M$, $\bar\lambda_M:M\to U_AM$, $\rho_M:MU_B\to M$, and $\bar\rho_M:M\to MU_B$, all with identity vertical boundaries for $M\in H(A,B)$. Fix any objects $A,B$, morphism $f:A\to B$, horizontal arrows $M\in H(A,B)$, $N\in H(B,A)$, and supplied structures $c,j$ consisting respectively of squares

$$\begin{gathered} u_c\in C_{1_A,f}(U_A,M),\qquad e_c\in C_{f,1_B}(M,U_B),\\ u_j\in C_{f,1_A}(U_A,N),\qquad e_j\in C_{1_B,f}(N,U_B) \end{gathered}$$

satisfying

$$\begin{gathered} u_c;e_c\doteq U_f,\qquad \bigl(\bar\lambda_M;(u_c\otimes e_c)\bigr);\rho_M=1_M,\\ u_j;e_j\doteq U_f,\qquad \bigl(\bar\rho_N;(e_j\otimes u_j)\bigr);\lambda_N=1_N. \end{gathered}$$

The defined base coevaluation is the square

$$\bar\lambda_{U_A};(u_c\otimes u_j) \;\in\; C_{1_A,1_A}(U_A,MN),$$

obtained by first applying the specified square $U_A\to U_AU_A$, then horizontally composing $u_c$ with $u_j$. No coherence assumption on $D$ is required, and $f$ may be an identity.

QAlgorithms.Papers.Independent.Intakethird100.P60.baseEvaluation

Let $V$ be any category and $D$ any of the specified double data, with arbitrary universe sizes. Write $H(A,B)$ for its horizontal-arrow types, $C_{f,g}(M,N)$ for squares with vertical boundaries $f,g$, $U_A$ for horizontal units, $MN$ for horizontal multiplication, $1_M$ for identity squares, $U_f$ for the chosen square on horizontal units with both vertical boundaries $f$, and $\otimes$ for horizontal square composition. Write $s;t$ for vertical composition in that order, with identity boundary composites simplified when appropriate, and $\doteq$ for heterogeneous equality. The specified unit squares are $\lambda_M:U_AM\to M$, $\bar\lambda_M:M\to U_AM$, $\rho_M:MU_B\to M$, and $\bar\rho_M:M\to MU_B$, all with identity vertical boundaries for $M\in H(A,B)$. Fix any objects $A,B$, morphism $f:A\to B$, horizontal arrows $M\in H(A,B)$, $N\in H(B,A)$, and supplied structures $c,j$ consisting respectively of squares

$$\begin{gathered} u_c\in C_{1_A,f}(U_A,M),\qquad e_c\in C_{f,1_B}(M,U_B),\\ u_j\in C_{f,1_A}(U_A,N),\qquad e_j\in C_{1_B,f}(N,U_B) \end{gathered}$$

satisfying

$$\begin{gathered} u_c;e_c\doteq U_f,\qquad \bigl(\bar\lambda_M;(u_c\otimes e_c)\bigr);\rho_M=1_M,\\ u_j;e_j\doteq U_f,\qquad \bigl(\bar\rho_N;(e_j\otimes u_j)\bigr);\lambda_N=1_N. \end{gathered}$$

The defined base evaluation is the square

$$(e_j\otimes e_c);\lambda_{U_B} \;\in\; C_{1_B,1_B}(NM,U_B),$$

obtained by horizontally composing $e_j$ with $e_c$, then applying the specified square $U_BU_B\to U_B$. No coherence assumption on $D$ is required, and $f$ may be an identity.

QAlgorithms.Papers.Independent.Intakethird100.P60.thinDoubleCoherence

For every category $V$, with arbitrary object and morphism universe sizes, take the double data in which each horizontal-arrow type $H(A,B)$ and each square type $C_{f,g}(M,N)$ is the lowest-universe singleton $\{\ast\}$, and every unit, product, square, and composition operation returns $\ast$. This definition supplies proofs of the following coherence requirements for those data. Write $U_A$ for horizontal units, $MN$ for horizontal products, $1_M$ for identity squares, $U_f$ for squares on horizontal units, $s;t$ for vertical composition in that order, and $s\otimes t$ for horizontal square composition; for identity-boundary squares, simplify composites of identity morphisms in $s;t$. Write $\alpha:(MN)P\to M(NP)$, $\bar\alpha$ for the specified reverse square, and $\lambda_M:U_AM\to M$, $\bar\lambda_M:M\to U_AM$, $\rho_M:MU_B\to M$, $\bar\rho_M:M\to MU_B$ for the specified unit squares. Write $\doteq$ for heterogeneous equality. Universally over all objects, morphisms, horizontal arrows, and squares making each expression well-typed, the supplied requirements are

$$\begin{gathered} (a;b);c\doteq a;(b;c),\qquad 1_M;a\doteq a,\qquad a;1_N\doteq a,\\ U_{1_A}=1_{U_A},\qquad U_{g\circ f}=U_f;U_g,\qquad 1_M\otimes1_N=1_{MN},\\ (a\otimes b);(c\otimes d)=(a;c)\otimes(b;d),\\ \alpha_{M,N,P};\bar\alpha_{M,N,P}=1_{(MN)P},\qquad \bar\alpha_{M,N,P};\alpha_{M,N,P}=1_{M(NP)},\\ \lambda_M;\bar\lambda_M=1_{U_AM},\qquad \bar\lambda_M;\lambda_M=1_M,\\ \rho_M;\bar\rho_M=1_{MU_B},\qquad \bar\rho_M;\rho_M=1_M,\\ ((a\otimes b)\otimes c);\alpha_{Q,R,S} \doteq \alpha_{M,N,P};(a\otimes(b\otimes c)),\\ (U_f\otimes a);\lambda_N\doteq\lambda_M;a,\qquad (a\otimes U_g);\rho_N\doteq\rho_M;a,\\ \bigl((\alpha_{M,N,P}\otimes1_Q);\alpha_{M,NP,Q}\bigr); (1_M\otimes\alpha_{N,P,Q}) =\alpha_{MN,P,Q};\alpha_{M,N,PQ},\\ \alpha_{M,U_B,N};(1_M\otimes\lambda_N) =\rho_M\otimes1_N. \end{gathered}$$

Here the associativity-naturality equation uses squares $a:M\to Q$, $b:N\to R$, $c:P\to S$ with matching adjoining vertical boundaries, and the unit-naturality equations use a square $a:M\to N$ with vertical boundaries $f,g$. Every compared square is the unique singleton element. If $V$ is empty, the universally indexed requirements are vacuous.

QAlgorithms.Papers.Independent.Intakethird100.P60.thinDoubleData

For every category $V$, with arbitrary object and morphism universe sizes, this definition supplies double data as follows. For every pair of objects $A,B$, the horizontal-arrow type $H(A,B)$ is the singleton type $\{\ast\}$; for every four objects, every suitably typed pair of vertical morphisms $f,g$, and every suitably typed pair of horizontal arrows $M,N$, the square type $C_{f,g}(M,N)$ is also $\{\ast\}$. Both kinds of singleton types lie in the lowest type universe. Every horizontal unit, every horizontal product, every identity square, every vertical composite, every square on horizontal units associated to a vertical morphism, every horizontal composite of squares, every associativity square in either direction, and every left or right unit square in either direction is defined to be $\ast$, for all admissible arguments. Thus every horizontal-arrow type and every square type that can be indexed is inhabited by exactly one element. The category $V$ may be empty, in which case all object-indexed specifications are vacuous.