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	|- 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 } ) ) >. )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cswapf	|- swapF
1		vc	|- c
2		cvv	|- _V
3		vd	|- d
4	1	cv	|- c
5		cxpc	|- Xc.
6	3	cv	|- d
7	4 6 5	co	|- ( c Xc. d )
8		vs	|- s
9		cbs	|- Base
10	8	cv	|- s
11	10 9	cfv	|- ( Base ` s )
12		vb	|- b
13		chom	|- Hom
14	10 13	cfv	|- ( Hom ` s )
15		vh	|- h
16		vx	|- x
17	12	cv	|- b
18	16	cv	|- x
19	18	csn	|- { x }
20	19	ccnv	|- `' { x }
21	20	cuni	|- U. `' { x }
22	16 17 21	cmpt	|- ( x e. b |-> U. `' { x } )
23		vu	|- u
24		vv	|- v
25		vf	|- f
26	23	cv	|- u
27	15	cv	|- h
28	24	cv	|- v
29	26 28 27	co	|- ( u h v )
30	25	cv	|- f
31	30	csn	|- { f }
32	31	ccnv	|- `' { f }
33	32	cuni	|- U. `' { f }
34	25 29 33	cmpt	|- ( f e. ( u h v ) |-> U. `' { f } )
35	23 24 17 17 34	cmpo	|- ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) )
36	22 35	cop	|- <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >.
37	15 14 36	csb	|- [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >.
38	12 11 37	csb	|- [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b |-> U. `' { x } ) , ( u e. b , v e. b |-> ( f e. ( u h v ) |-> U. `' { f } ) ) >.
39	8 7 38	csb	|- [_ ( 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 } ) ) >.
40	1 3 2 2 39	cmpo	|- ( 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 } ) ) >. )
41	0 40	wceq	|- 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 } ) ) >. )