Different Notions of \( 2 \)-Categories
Table of Contents
- 1. Strict \( 2 \)-Categories
- 2. (Weak) \(2 \)-Categories or Bicategories
The notion ``\( 2 \)-category’’ is overloaded and can mean different things:
- strict \( 2 \)-category (historically hypercategory)
- weak \( 2 \)-category (bicategory)
- double category
- general \( 2 \)-category
- \( (\infty, 2) \)-category
To reduce ambiguity we fix that ``\( 2 \)-category’’ we means ``weak \( 2 \)-category’’ (= bicategory) (in almost all cases).
Here we give precise define what strict \( 2 \)-categories and weak \( 2 \)-categories are. In short we can say that the notion of \( (\infty, 2) \)-categories is the most general notion. It specializes to the notion of general \( 2 \)-categories by assuming that the only \( n \)-morphisms are identities for \( n \ge 3 \). There can be different models of \( (\infty,2) \)-categories, hence there can potentially be different models of general \( 2 \)-categories. ``Weak \( 2 \)-category’’ and ``bicategory’’ mean the same thing. They are an explicit model of general \( 2 \)-categories. The notion of strict \( 2 \)-categories is a specialization of the notion of weak \( 2 \)-categories by assuming that all higher coherent laws are witnessed by identities.
To reduce ambiguity we fix that ``\( 2 \)-category’’ we means ``weak \( 2 \)-category’’ (= bicategory) (in almost all cases).
1. Strict \( 2 \)-Categories
The notion of a strict \( 2 \)-category is the simplest notion, because all higher coherent laws are equalities. There are several (slightly) different but equivalent definitions one can give:
- explicit definition using horizontal composition,
- explicit definition using left and right whiskerings,
- a \( \Cat \)-enriched category,
- definition using sesquicategories,
- definition using only \( 2 \)-morphisms.
1.1. Explicit definition using horizontal composition.
We start with the explicit definition using horizontal composition, as we think this is the most natural definition.
A strict \( 2 \)-category \( \mathcal C \) consists of things:
- a collection \( \Ob(\mathcal C) \) of objects (\( 0 \)-morphisms or \( 0 \)-cells),
- a collection \( \mathcal C(a,b) \) of \( 1 \)-morphisms (or \( 1 \)-cells) for every \( a,b \in \Ob(\mathcal C) \),
- a collection \( 2 \mathcal C(f,g) \) (or just \( \mathcal C(f,g) \)) of \( 2 \)-morphisms (or \( 2 \)-cells) for every \( 1 \)-morphisms \( f,g \),
that is equipped with structure/data:
- an identity \( 1 \)-morphism \( 1_a \colon a \rightarrow a \) for every object \( a \),
- an identity \( 2 \)-morphism \( 1_f \colon f \Rightarrow f \) for every \( 1 \)-morphism \( f \),
- a composite \( g \circ f \colon a \rightarrow c \) for every \( 1 \)-morphisms \( f \colon a \rightarrow b \) and \( g \colon b \rightarrow c \),
- a vertical composite \( \beta \circ \alpha \colon f \Rightarrow h \) for every \( 2 \)-morphisms \( \alpha \colon f \Rightarrow g \) and \( \beta \colon g \Rightarrow h \),
- a horizontal composite \( \beta \bullet \alpha \colon i \circ f \Rightarrow j \circ g \) for every \( 2 \)-morphisms \( \alpha \colon f \Rightarrow g \colon a \rightarrow b \) and \( \beta \colon i \Rightarrow j \colon b \rightarrow c \),
that satisfies
- unital axioms:
- \( f \circ 1_a = f = 1_b \circ f \) for every \( f \colon a \rightarrow b \),
- \( \alpha \circ 1_f = \alpha = 1_g \circ \alpha \) for every \( \alpha \colon f \Rightarrow g \),
- \( \alpha \bullet 1_f = \alpha = 1_g \bullet \alpha \) for every \( \alpha \colon f \Rightarrow g \),
- associativity:
- \( h \circ (g \circ f) = (h \circ g) \circ f \)
for every \( f \colon a \rightarrow b \), \( g \colon b \rightarrow c \) and \( h \colon c \rightarrow d \), - \( \gamma \circ (\beta \circ \alpha) = (\gamma \circ (\beta \circ \alpha) \)
for every \( \alpha \colon f \Rightarrow g \), \( \beta \colon g \Rightarrow h \) and \( \gamma \colon h \Rightarrow i \), - \( \gamma \bullet (\beta \bullet \alpha) = (\gamma \bullet \beta) \bullet \alpha \)
for every \( \alpha \colon f \Rightarrow g \), \( \beta : i \Rightarrow h \) and \( \gamma \colon k \Rightarrow l \) with \( f,g \colon a \rightarrow b \) and \( i,h \colon b \rightarrow c \) and \( k,l \colon c \rightarrow d \)
- \( h \circ (g \circ f) = (h \circ g) \circ f \)
- interchange law: \( (\beta ' \circ \beta ) \bullet (\alpha ' \circ \alpha) = (\beta ' \bullet \alpha ') \circ (\beta \bullet \alpha) \)
for every \( \alpha \colon f \Rightarrow g, \alpha ' \colon g \Rightarrow h \) and \( \beta \colon i \Rightarrow j, \beta ' \colon j \Rightarrow k \) and \( f,g,h \colon a \rightarrow b \) and \( i,j,k \colon b \rightarrow c \).
In words: to give strict \( 2 \)-category is to give objects, \( 1 \)-morphisms and \( 2 \)-morphisms (only between \( 1 \)-morphisms with same source and target) and to specify identity \( 1 \)- and \( 2 \)-morphisms, composition of \( 1 \)-morphisms, and vertical and horizontal composition of \( 2 \)-morphisms such that all compositions are compatible with the identities, associative and the interchange law holds.
If we look at string diagrams, these axioms become intuitive. By this we mean: the list of axioms is equivalent to the statement ``string diagrams are well-defined’’. See 1.6 for string diagrams.
Another thing: in the above definition we used wrongly (!) “\(\bullet \)” to denote the horizontal composition. Better notation is to use “\(\circ \)” for (normal) composition and horizontal composition and “\(\bullet \)” for vertical composition, because horizontal composition induces (normal) composition. Hence we should use the same symbol for both of them.
We define some basic notions.
Let \( \mathcal C\) be a strict \( 2\)-category. Let \( f \colon a \rightarrow b, i \colon c \rightarrow d \) be \( 1 \)-morphisms and \( \alpha \colon g \rightarrow h \) a \( 2 \)-morphism with \( g,h \colon b \rightarrow c \). Then the left whiskering \( \alpha \triangleleft f \colon g \circ f \Rightarrow h \circ f \) of \( f \) and \( \alpha \) is \( \alpha \triangleleft f := \alpha \bullet 1_f \). The right whiskering \( i \triangleright \alpha \colon i \circ g \Rightarrow i \circ h \) of \( i \) and \( \alpha \) is \( i \triangleright \alpha := 1_i \bullet \alpha \).
Before we discuss what relation are satisfied by whiskerings, we visualize the different compositions by diagrams.
Let \( \mathcal C \) be a strict \( 2 \)-category. The composition of \( 1 \)-morphisms is visualized by
\begin{equation*} \xymatrix{ A \ar@{->}[r]^{f} & B \ar@{->}[r]^{g} & C } \mapsto \xymatrix{ A \ar@{->}[r]^{g \circ f} & C } \end{equation*}The vertical composition of \( 2\)-morphisms is visualized by
\begin{equation*} \xymatrix{ A \ar@/^1.5pc/[rr]^{f}="1" \ar@/_1.5pc/[rr]_{h}="2" \ar[rr]|-{g}="3" && B \ar@{=>}"1" ;"3"^\alpha \ar@{=>}"3";"2"^\beta } \mapsto \xymatrix{ A \ar@/^1.5pc/[rr] ^{f}="1" \ar@/_1.5pc/[rr]_h="2" && B \ar@{=>}"1";"2" ^{\beta \circ \alpha } } \end{equation*}The horizontal composition of \( 2 \)-morphisms is visualized by
\begin{equation*} \xymatrix{ A \ar@/^1.5pc/[rr] ^{f}="1" \ar@/_1.5pc/[rr] _{g}="2" && B \ar@/^1.5pc/[rr] ^{h}="3" \ar@/_1.5pc/[rr] _{i}="4" && C \ar@{=>}"1";"2"^\alpha \ar@{=>}"3";"4"^\beta } \mapsto \xymatrix{ A \ar@/^1.5pc/[rr] ^{h \circ f}="1" \ar@/_1.5pc/[rr] _{i \circ g}="2" && B \ar@{=>}"1";"2" ^{\beta \bullet \alpha } } \end{equation*}Left whiskering is visualized by
\begin{equation*} \xymatrix{ A \ar[rr]^f && B \ar@/^1.5pc/[rr] ^{g}="1" \ar@/_1.5pc/[rr] _{h}="2" && C \ar@{=>}"1";"2"^\alpha } \mapsto \xymatrix{ A \ar@/^1.5pc/[rr] ^{g \circ f}="1" \ar@/_1.5pc/[rr] _{h \circ f}="2" && C \ar@{=>}"1";"2" ^{\alpha \triangleleft f} } \end{equation*}The right whiskering is visualized by
\begin{equation*} \xymatrix{ A \ar@/^1.5pc/[r] ^{f}="1" \ar@/_1.5pc/[r] _{g}="2" & B \ar[r]^h & C \ar@{=>}"1";"2"^\alpha } \mapsto \xymatrix{ A \ar@/^1.5pc/[r] ^{h \circ f}="1" \ar@/_1.5pc/[r] _{h \circ g}="2" & C \ar@{=>}"1";"2" ^{h \triangleright \alpha } } \end{equation*}The associativity laws say that the following diagrams are well-defined:
\begin{equation*} \xymatrix{ A \ar[r] & B \ar[r] & C \ar[r] & D, } \xymatrix{ A \ar@/^2pc/[rr]^{}="1" \ar@/^0.66pc/[rr]^{}="2" \ar@/_0.66pc/[rr]^{}="3" \ar@/_2pc/[rr]^{}="4" && B, \ar@{=>}"1";"2" \ar@{=>}"2";"3" \ar@{=>}"3";"4" } \xymatrix{ A \ar@/^1.5pc/[r]^{}="1" \ar@/_1.5pc/[r]^{}="2" & B \ar@/^1.5pc/[r]^{}="3" \ar@/_1.5pc/[r]^{}="4" & C \ar@/^1.5pc/[r]^{}="5" \ar@/_1.5pc/[r]^{}="6" & D \ar@{=>}"1";"2" \ar@{=>}"3";"4" \ar@{=>}"5";"6" } \end{equation*}The interchange law states that
\begin{equation*} \xymatrix{ A \ar@/^1.5pc/[rr]^{}="1" \ar[rr]^{}="2" \ar@/_1.5pc/[rr]^{}="3" && B \ar@/^1.5pc/[rr]^{}="4" \ar[rr]^{}="5" \ar@/_1.5pc/[rr]^{}="6" && C \ar@{=>}"1";"2" \ar@{=>}"2";"3" \ar@{=>}"4";"5" \ar@{=>}"5";"6" } \end{equation*}is well-defined.
Next we prove some coherent laws for whiskerings.
Let \( \mathcal C \) be a strict \( 2 \)-category. Then whiskering satisfies unital axioms:
- \( 1_g \triangleleft f = 1 _{g \circ f} \)
- \( g \triangleright 1_f = 1 _{g \circ f} \)
and associativity axioms:
- \( i \triangleright (\alpha \triangleleft f) = (i \triangleright \alpha) \triangleleft f \)
- \( \alpha \triangleleft (g \circ f) = (\alpha \triangleleft g) \triangleleft f \)
- \( (i \circ h) \triangleright \alpha = i \triangleright (h \triangleright \alpha) \)
and distributive axioms:
- \( (\beta \circ \alpha) \triangleleft f = (\beta \triangleleft f) \circ (\alpha \triangleleft f) \)
- \( i \triangleright (\beta \circ \alpha) = (i \triangleright \beta) \circ (i \triangleright \alpha) \)
and satisfies: \( \beta \bullet \alpha = (\beta \triangleleft g) \circ (h \triangleright \alpha) = (i \triangleright \alpha) \circ (\beta \triangleleft f)\)
1.2. Explicit definition using left and right whiskerings.
definition of left and right whiskerings, alternative definition of strict \( 2 \)-categories via vertical composition and left/right whiskerings (check axioms list above via this second definition). It seems like composition and vertical composition are more fundamental than horizontal composition (compare to cubical \( 2 \)-sets)
Instead of taking horizontal composition as part of the data, we can take left and right whiskerings to be data. Then we can construct horizontal composition, like we constructed left and right whiskerings in 1.1 Both definitions are equivalent.
A strict \( 2 \)-category \( \mathcal C \) consists of things:
- a collection \( \Ob(\mathcal C) \) of objects (\( 0 \)-morphisms or \( 0 \)-cells),
- a collection \( \mathcal C(a,b) \) of \( 1 \)-morphisms (or \( 1 \)-cells) for every \( a,b \in \Ob(\mathcal C) \),
- a collection \( 2 \mathcal C(f,g) \) (or just \( \mathcal C(f,g) \)) of \( 2 \)-morphisms (or \( 2 \)-cells) for every \( 1 \)-morphisms \( f,g \),
that is equipped with structure/data:
- an identity \( 1 \)-morphism \( 1_a \colon a \rightarrow a \) for every object \( a \),
- an identity \( 2 \)-morphism \( 1_f \colon f \Rightarrow f \) for every \( 1 \)-morphism \( f \),
- a composite \( g \circ f \colon a \rightarrow c \) for every \( 1 \)-morphisms \( f \colon a \rightarrow b \) and \( g \colon b \rightarrow c \),
- a vertical composite \( \beta \circ \alpha \colon f \Rightarrow h \) for every \( 2 \)-morphisms \( \alpha \colon f \Rightarrow g \) and \( \beta \colon g \Rightarrow h \),
- a left whiskering \( \alpha \triangleleft f \colon g \circ f \Rightarrow h \circ f \) for every \( \alpha \colon g \Rightarrow h \) and \( f \colon a \rightarrow b \) and \( g,h \colon b \rightarrow c \),
- a right whiskering \( h \triangleright \alpha \colon h \circ f \Rightarrow h \circ g \) for every \( \alpha \colon f \Rightarrow g \) and \( h \colon b \rightarrow c \) and \( f,g \colon a \rightarrow b \),
that satisfies
- unital axioms:
- \( f \circ 1_a = f = 1_b \circ f \) for every \( f \colon a \rightarrow b \),
- \( \alpha \circ 1_f = \alpha = 1_g \circ \alpha \) for every \( \alpha \colon f \Rightarrow g \),
- \( 1_g \triangleleft f = 1 _{g \circ f} = g \triangleright 1_f \) for every \( f \colon a \rightarrow b \) and \( g \colon b \rightarrow c \),
- associativity:
- \( h \circ (g \circ f) = (h \circ g) \circ f \)
for every \( f \colon a \rightarrow b \), \( g \colon b \rightarrow c \) and \( h \colon c \rightarrow d \), - \( \gamma \circ (\beta \circ \alpha) = (\gamma \circ (\beta \circ \alpha) \)
for every \( \alpha \colon f \Rightarrow g \), \( \beta \colon g \Rightarrow h \) and \( \gamma \colon h \Rightarrow i \), - \( i \triangleright (\alpha \triangleleft f) = (i \triangleright \alpha) \triangleleft f \),
- \( \alpha \triangleleft (g \circ f) = (\alpha \triangleleft g) \triangleleft f \),
- \( (i \circ h) \triangleright \alpha = i \triangleright (h \triangleright \alpha) \),
- \( h \circ (g \circ f) = (h \circ g) \circ f \)
- distributive axioms:
- \( (\beta \circ \alpha) \triangleleft f = (\beta \triangleleft f) \circ (\alpha \triangleleft f) \),
- \( i \triangleright (\beta \circ \alpha) = (i \triangleright \beta) \circ (i \triangleright \alpha) \),
- compatibility axioms: \((\beta \triangleleft g) \circ (h \triangleright \alpha) = (i \triangleright \alpha) \circ (\beta \triangleleft f)\)
Let \( \mathcal C \) be a strict \( 2 \)-category. The horizontal composition \( \beta \bullet \alpha \) of \( \alpha \) and \( \beta \) is \( \beta \bullet \alpha := (\beta \triangleleft g) \circ (h \triangleright \alpha)\).
1.2.1. TODO Show that explicit definitions are equivalent.
1.3. Explicit least data definition.
In the explicit definition using horizontal composition the composition of \( 1 \)-morphisms is redundant data. Following the paradigm of least data, we give an explicit definition using vertical composition and horizontal composition but not composition of \( 1 \)-morphisms.
A strict \( 2 \)-category \( \mathcal C \) consists of things:
- a collection \( \Ob(\mathcal C) \) of objects (\( 0 \)-morphisms or \( 0 \)-cells),
- a collection \( \mathcal C(a,b) \) of \( 1 \)-morphisms (or \( 1 \)-cells) for every \( a,b \in \Ob(\mathcal C) \),
- a collection \( 2 \mathcal C(f,g) \) (or just \( \mathcal C(f,g) \)) of \( 2 \)-morphisms (or \( 2 \)-cells) for every \( 1 \)-morphisms \( f,g \),
that is equipped with structure/data:
- an identity \( 1 \)-morphism \( 1_a \colon a \rightarrow a \) for every object \( a \),
- an identity \( 2 \)-morphism \( 1_f \colon f \Rightarrow f \) for every \( 1 \)-morphism \( f \),
- a vertical composite \( \beta \circ \alpha \colon f \Rightarrow h \) for every \( 2 \)-morphisms \( \alpha \colon f \Rightarrow g \) and \( \beta \colon g \Rightarrow h \),
- a horizontal composite \( \beta \bullet \alpha \) for every \( 2 \)-morphisms \( \alpha \colon f \Rightarrow g \colon a \rightarrow b \) and \( \beta \colon i \Rightarrow j \colon b \rightarrow c \),
that satisfies
- source-target axiom: Source and target of \( \beta \bullet \alpha \) are \( 1 \)-morphisms from \( a \) to \( c \)
- unital axioms:
- \( \alpha \circ 1_f = \alpha = 1_g \circ \alpha \) for every \( \alpha \colon f \Rightarrow g \),
- \( \alpha \bullet 1_f = \alpha = 1_g \bullet \alpha \) for every \( \alpha \colon f \Rightarrow g \),
- associativity:
- \( \gamma \circ (\beta \circ \alpha) = (\gamma \circ (\beta \circ \alpha) \)
for every \( \alpha \colon f \Rightarrow g \), \( \beta \colon g \Rightarrow h \) and \( \gamma \colon h \Rightarrow i \), - \( \gamma \bullet (\beta \bullet \alpha) = (\gamma \bullet \beta) \bullet \alpha \)
for every \( \alpha \colon f \Rightarrow g \), \( \beta : i \Rightarrow h \) and \( \gamma \colon k \Rightarrow l \) with \( f,g \colon a \rightarrow b \) and \( i,h \colon b \rightarrow c \) and \( k,l \colon c \rightarrow d \)
- \( \gamma \circ (\beta \circ \alpha) = (\gamma \circ (\beta \circ \alpha) \)
- interchange law: \( (\beta ' \circ \beta ) \bullet (\alpha ' \circ \alpha) = (\beta ' \bullet \alpha ') \circ (\beta \bullet \alpha) \)
for every \( \alpha \colon f \Rightarrow g, \alpha ' \colon g \Rightarrow h \) and \( \beta \colon i \Rightarrow j, \beta ' \colon j \Rightarrow k \) and \( f,g,h \colon a \rightarrow b \) and \( i,j,k \colon b \rightarrow c \).
We can reconstruct composition of \( 1 \)-morphisms by defining \( g \circ f \) to be the source (or target) of \( 1_g \bullet 1_f \). Associativity follows from associativity of horizontal composition, the unital axiom follows from the unital axiom of horizontal composition.
1.4. Definition using enrichment.
A strict \( 2 \)-category a \( \Cat \)-enriched category.
Explicitly this means a strict \( 2 \)-category \( \mathcal C \) consists of the following data:
- a class \( \Ob(\mathcal C) \) of objects and
- a hom-category \( \mathcal C(a,b) \) for every objects \( a,b \) and
- a functor \( 1_a \colon \boldsymbol 1 \rightarrow \mathcal C(a,a) \) specifying the identity of \( a \) for every object \( a \) and
- a functor \(\comp _{a,b,c} \colon \mathcal C(b,c) \times \mathcal C(a,b) \rightarrow \mathcal C(a,c) \) specifying composition for every objects \( a,b,c \)
that satisfies the following properties:
for every objects \( a,b,c,d \) the diagram
\begin{equation*} \begin{tikzcd} (\mathcal C(c,d) \times \mathcal C(b,c)) \times \mathcal C(a,b) \ar[rr, "\cong \text{(associator of \( \times \))}"] \ar[d, "\comp _{b,c,d} \times \id _{\mathcal C(a,b)}"] & & \mathcal C(c,d) \times (\mathcal C(b,c) \times \mathcal C(a,b)) \ar[d, swap, "\id _{\mathcal C(c,d)} \times \comp _{a,b,c}"]\\ \mathcal C(b,d) \times \mathcal C(a,b) \ar[r, swap, "\comp _{a,b,d}"] & \mathcal C(a,d) & \mathcal C(c,d) \times \mathcal C(a,c) \ar[l, "\comp _{a,c,d}"] \end{tikzcd} \end{equation*}commutes (composition is strictly associative).
for every objects \( a,b \) the diagram
\begin{equation*} \begin{tikzcd}[column sep=huge] \mathcal C(b,b) \times \mathcal C(a,b) \ar[r, "\comp _{a,b,b}"] & \mathcal C(a,b) & \mathcal C(a,b) \times \mathcal C(a,a) \ar[l, swap, "\comp _{a,a,b}"] \\ \boldsymbol 1 \times \mathcal C(a,b) \ar[ru, swap, "l _{\mathcal C(a,b)}"] \ar[u, "1_b \times \id _{\mathcal C(a,b)}"] & & \mathcal C(a,b) \times \boldsymbol 1 \ar[u, swap, "\id _{\mathcal C(a,b)} \times 1_a"] \ar[lu, "r _{\mathcal C(a,b)}"] \end{tikzcd} \end{equation*}commutes (composition is strictly unital).
We reconstruct
- composition of \( 1 \)-morphisms as given by \( \comp \),
- vertical composition as given by the composition in the hom-categories \( \mathcal C(a,b)\),
- horizontal composition as given by \( \comp(\beta, \alpha) \) for two \( 2 \)-morphisms \( \alpha, \beta \).
1.5. SOMEDAY Definition only using \( 2 \)-morphisms.
Remember the definition of a \( 1 \)-category using only arrows (identify an object with its identity morphism). We can do the same trick for \( 2 \)-categories by identifying an object with its identity \( 1 \)-morphisms and a \( 1 \)-morphism with its identity \( 2 \)-morphism. We have to slightly alter the explicit least data definition in 1.3, because we have to ensure that only ``composable’’ \( 2 \)-morphisms are actually composed.
1.6. TODO String diagrams for strict \( 2 \)-categories.
2. (Weak) \(2 \)-Categories or Bicategories
2.1. Definition using enrichment
A (weak) \(2 \)-category (or bicategory) \(\mathcal C \) consists of
- a collection \(\Ob \mathcal C \) of objects (0-cells),
- a category \(\mathcal C(x,y) \) for objects \(x,y \),
- an identity \(1 \)-morphism \(1_x \in \mathcal C(x,x) \) for every object \( x \)
- a functor \(\circ \colon \mathcal C(y,z) \times \mathcal C(x,y) \rightarrow \mathcal C(x,z) \) for all objects \( x, y, z \) (horizontal composition),
- natural isomorphisms \( - \circ 1_x \Rightarrow \id _{\mathcal C(x,y)}\) and \(1_y \circ - \Rightarrow \id _{\mathcal C(x,y)} \) for all objects \(x,y \) (unitors),
- a natural isomorphism
for all objects \(w,x,y,z \), such that
- the pentagram axioms holds
for all \( 1\)-morphisms \(v \xrightarrow f w \xrightarrow g x \xrightarrow h y \xrightarrow i z \),
- the unital axioms holds
for all \(1 \)-morphisms \(x \xrightarrow f y \xrightarrow g z \).
2.2. QUESTION Is a weak \(2 \)-category a \(\operatorname{weakCat} \)-enriched category? If not, what are the differences?
2.3. General (Weak) \(2 \)-Categories
We want to develop a notion of a “truly weak” \( 2 \)-category. By this we mean a notion of a \(2 \)-category where composition itself is only well-defined up to isomorphism (or higher coherence).
Let’s start with the idea that the higher structure (here composition of \(2 \)-morphisms) should still be strictly well-defined and only the composition of \(1 \)-morphisms should be well-defined up to isomorphism. Hence our idea is to use an almost functor to encode the composition.