prove that total saturated anabicats closed under taking products
Summary
Let\
- $\mathcal{A}, \mathcal{B}: S \rightarrow \text{Set}$ be total sanabicats. Then $\mathcal{A} \times \mathcal{B}$ is a total sanabicat.
(proof)(sketch)\
Let $(A,B) \in (\mathcal{A} \times \mathcal{B})(C_0)$.\
- As $\mathcal{A}$ and $\mathcal{B}$ are total, there exist $s \in \text{ID}\mathcal{A}(A)$ and $t \in \text{ID}\mathcal{A}(A)$; i.e.\
-- $s \in |\text{id}|_\mathcal{A}$\
-- $t \in |\text{id}|_\mathcal{B}$\
-- $s_1\text{id}_1(s)=A$\
-- $s_1\text{id}_1(t)=B$\
- Then\
-- there exists $(s,t) \in |\text{id}|_{\mathcal{A} \times \mathcal{B}}$\
-- such that $s_1\text{id}1(s,t)=(s1\text{id}1(s), s1\text{id}_1(t))=(A,B)$\
Let\
- $(A,B), (A',B'), (A'', B'') \in (\mathcal{A} \times \mathcal{B})(C_0)$\
- $(f,g): (A,B) \rightarrow (A',B'), (f',g'): (A',B') \rightarrow (A'',B'') \in (\mathcal{A} \times \mathcal{B})(C_1)$\
Then\
- As $\mathcal{A}$ and $\mathcal{B}$ are total, there exist\
-- $u \in |\circ|_\mathcal{A}$\
-- $v \in |\circ|_\mathcal{B}$, such that\
-- $l_\circ(u)=f, r_\circ(u)=f', c_\circ(u)=f''$ for some $f'': A \rightarrow A''$\
-- $l_\circ(v)=g, r_\circ(v)=g', c_\circ(v)=g''$ for some $g'': B \rightarrow B''$\
- Then there exists $(u, v) \in |\circ|_{\mathcal{A} \times \mathcal{B}}$ such that\
-- $l_\circ(u,v)=(l_\circ(u), l_\circ(v))=(f,g)$\
-- $r_\circ(u,v)=(r_\circ(u), r_\circ(v))=(f',g')$\
-- $c_\circ(u,v)=(c_\circ(u), c_\circ(v))=(f'',g'')$\
prove that we don't have to deal with isos wrt associators (and unitors)
Summary
(lemma)\
Let\
- $\mathcal{A}: S \rightarrow \text{Set}$ be a partial sanabicat\
- $A, B \in \mathcal{A}(C_0)$\
- $s \in \text{ID}_\mathcal{A}(A)$\
- $t \in \text{ID}_\mathcal{A}(A)$\
- $f: A \rightarrow B$.\
(i) Then there exists some $u' \in \text{COMP}\mathcal{A}(\text{id}1(s), f, f)$.
(proof)(sketch)\
As $\mathcal{A}$ is total, there exists some $h: A \rightarrow B$ and $u \in \text{COMP}\mathcal{A}(\text{id}1(s), f, h)$.\
- There is an isomorphism $\text{lUtor}(f, s, u): h \implies f$. By saturation (via a theorem by makkai), (i) is true\
Similarly, (ii) there exists some $u' \in \text{COMP}\mathcal{A}(f, \text{id}1(t), f)$.\
(lemma)\
Let\
- $\mathcal{A}: S \rightarrow \text{Set}$ be a partial sanabicat\
- $A, B, C, D \in \mathcal{A}(C_0)$\
- $f: A \rightarrow B$\
- $g: B \rightarrow C$\
- $h: C \rightarrow D$\
- $j: A \rightarrow C$\
- $k: B \rightarrow D$\
- $l: A \rightarrow D$\
- $u \in \text{COMP}_\mathcal{A}(f,g,j)$\
- $v \in \text{COMP}_\mathcal{A}(g, h, k)$\
- $w \in \text{COMP}_\mathcal{A}(f,k,l)$\
(iii) There exists some $z \in \text{COMP}_\mathcal{A}(j,h,l)$.
(proof)(sketch)\
As $\mathcal{A}$ is total, there exists some $l': A \rightarrow D$ and $z \in \text{COMP}_\mathcal{A}(j,h,l')$.\
- There exists an isomorphism $\text{Ator}(v, w, u, z): l \implies l'$\
- By saturation (via a theorem by makkai), (i) is true\
for inverse equivanences between total sanabicats, rigourously define a candidate mapping for 0-cells, 1-cells and 2-cells
Summary
(action on 0-cells)\
$(\forall B \in \mathcal{B}$, let $G(B)=A$ for some $A \in \mathcal{A}$ such that $F(A) \simeq B$\
(action on 1-cells)\
Let $B, B' \in \mathcal{B}(C_1)$ and $f \in \text{Hom}_{\mathcal{B}}(B, B')$.\
- There exist equivalences $e_B: FG(B) \rightarrow B$ and $e_{B'}: FG(B') \rightarrow B'$.\
- As $\mathcal{B}$ is total, there exists $s \in \text{ID}_\mathcal{B}(FG(B'))$.\
- As $e_{B'}$ is an equivalence, there exist $e_{B'}^{-1}: B' \rightarrow FG(B')$ and $u_{FG(B)} \in \text{COMP}\mathcal{B}(e{B'}, e_{B'}^{-1}, s)$\
- As $\mathcal{B}$ is total, there exist\
-- $w \in \text{COMP}\mathcal{B}(eB, f, h)$ for some $h: FG(B) \rightarrow B'$\
-- $w' \in \text{COMP}\mathcal{B}(h, e{B'}^{-1}, g)$ for some $g: FG(B) \rightarrow FG(B')$\
- As $F$ is essentially surjective on 1-cells, there exists some $g': G(B) \rightarrow G(B')$ and isomorphism $\alpha: F(g') \cong g$\
Let $G(f) = g'$. As $\mathcal{B}$ is saturated, there exists\
- $w'' \in \text{COMP}\mathcal{B}(h, e{B'}^{-1}, F(G(f))$ such that $\circ'(\text{id}2(h), \text{id}2(e_{B'}^{-1}), w'', w')=\alpha$\
(just define action on cells for now and worry about 'functoriality' etc later?)
(action on 2-cells)\
Let\
- $f, g \in \text{Hom}_\mathcal{B}(B, B')$\
- $\alpha \in \text{Hom}_\mathcal{B}(f, g)$\
- $\beta := \circ'(\circ'(\text{id}2(eB), \alpha, w, u), \text{id}2((eB')^{-1}), w'', u'')$ for $w, u, w'', u'' \in |\circ|$\
such that $c_{w''} = FG(f)$ and $c_{u''} = FG(g)$.\
- $\beta \in \text{Hom}_\mathcal{B}(FG(f), FG(g))$\
As $F$ is fully faithful, there exists some $\beta' \in \text{Hom}_\mathcal{A}(G(f), G(g))$ such that $F(\beta')=\beta$. We let $F(\alpha) = \beta'$\