Definition df-swapf

Description: Define the swap functor from ( C Xc. D ) to ( D Xc. C ) by swapping all objects ( swapf1 ) and morphisms ( swapf2 ) .

Such functor is called a "swap functor" in https://arxiv.org/pdf/2302.07810 or a "twist functor" in https://arxiv.org/pdf/2508.01886 , the latter of which finds its counterpart as "twisting map" in https://arxiv.org/pdf/2411.04102 for tensor product of algebras. The "swap functor" or "twisting map" is often denoted as a small tau ta in literature. However, the term "twist functor" is defined differently in https://arxiv.org/pdf/1208.4046 and thus not adopted here.

tpos _I depends on more mathbox theorems, and thus are not adopted here. See dfswapf2 for an alternate definition.

(Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Assertion	df-swapf	Could not format assertion : No typesetting found for |- swapF = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cswapf	Could not format swapF : No typesetting found for class swapF with typecode class
1		vc	$$setvarc$$
2		cvv	$$class\mathrm{V}$$
3		vd	$$setvard$$
4	1	cv	$$setvarc$$
5		cxpc	$$class{\times }_c$$
6	3	cv	$$setvard$$
7	4 6 5	co	$$class\left(c{\times }_{c}d\right)$$
8		vs	$$setvars$$
9		cbs	$$class\mathrm{Base}$$
10	8	cv	$$setvars$$
11	10 9	cfv	$$class{\mathrm{Base}}_s$$
12		vb	$$setvarb$$
13		chom	$$class\mathrm{Hom}$$
14	10 13	cfv	$$class\mathrm{Hom}\left(s\right)$$
15		vh	$$setvarh$$
16		vx	$$setvarx$$
17	12	cv	$$setvarb$$
18	16	cv	$$setvarx$$
19	18	csn	$$class\left\{x\right\}$$
20	19	ccnv	$$class{\left\{x\right\}}^{-1}$$
21	20	cuni	$$class\bigcup {\left\{x\right\}}^{-1}$$
22	16 17 21	cmpt	$$class\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
23		vu	$$setvaru$$
24		vv	$$setvarv$$
25		vf	$$setvarf$$
26	23	cv	$$setvaru$$
27	15	cv	$$setvarh$$
28	24	cv	$$setvarv$$
29	26 28 27	co	$$class\left(uhv\right)$$
30	25	cv	$$setvarf$$
31	30	csn	$$class\left\{f\right\}$$
32	31	ccnv	$$class{\left\{f\right\}}^{-1}$$
33	32	cuni	$$class\bigcup {\left\{f\right\}}^{-1}$$
34	25 29 33	cmpt	$$class\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
35	23 24 17 17 34	cmpo	$$class\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)$$
36	22 35	cop	$$class⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
37	15 14 36	csb	$$class⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
38	12 11 37	csb	$$class⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
39	8 7 38	csb	$$class⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
40	1 3 2 2 39	cmpo	$$class\left(c\in \mathrm{V},d\in \mathrm{V}⟼⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩\right)$$
41	0 40	wceq	Could not format swapF = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. ) : No typesetting found for wff swapF = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >. ) with typecode wff