Theorem tposcurf12

Description: The partially evaluated transposed curry functor at a morphism. (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Hypotheses	tposcurf1.g	No typesetting found for |- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
	tposcurf1.a	$$⊢A={\mathrm{Base}}_C$$
	tposcurf1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	tposcurf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	tposcurf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
	tposcurf1.x	$$⊢\phi \to X\in A$$
	tposcurf1.k	$$⊢\phi \to K=1^{st}\left(G\right)\left(X\right)$$
	tposcurf1.b	$$⊢B={\mathrm{Base}}_D$$
	tposcurf11.y	$$⊢\phi \to Y\in B$$
	tposcurf12.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	tposcurf12.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	tposcurf12.y	$$⊢\phi \to Z\in B$$
	tposcurf12.g	$$⊢\phi \to H\in \left(YJZ\right)$$
Assertion	tposcurf12	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Z\right)\left(H\right)=H\left(⟨Y,X⟩2^{nd}\left(F\right)⟨Z,X⟩\right)\underset{\dot{}}{1}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		tposcurf1.g	Could not format ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) : No typesetting found for |- ( ph -> G = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) with typecode |-
2		tposcurf1.a	$$⊢A={\mathrm{Base}}_C$$
3		tposcurf1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		tposcurf1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
5		tposcurf1.f	$$⊢\phi \to F\in \left(\left(D{\times }_{c}C\right)\mathrm{Func}E\right)$$
6		tposcurf1.x	$$⊢\phi \to X\in A$$
7		tposcurf1.k	$$⊢\phi \to K=1^{st}\left(G\right)\left(X\right)$$
8		tposcurf1.b	$$⊢B={\mathrm{Base}}_D$$
9		tposcurf11.y	$$⊢\phi \to Y\in B$$
10		tposcurf12.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
11		tposcurf12.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
12		tposcurf12.y	$$⊢\phi \to Z\in B$$
13		tposcurf12.g	$$⊢\phi \to H\in \left(YJZ\right)$$
14	1	fveq2d	Could not format ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ) : No typesetting found for |- ( ph -> ( 1st ` G ) = ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ) with typecode |-
15	14	fveq1d	Could not format ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) : No typesetting found for |- ( ph -> ( ( 1st ` G ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) with typecode |-
16	7 15	eqtrd	Could not format ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) : No typesetting found for |- ( ph -> K = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) with typecode |-
17	16	fveq2d	Could not format ( ph -> ( 2nd ` K ) = ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ) : No typesetting found for |- ( ph -> ( 2nd ` K ) = ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) ) with typecode |-
18	17	oveqd	Could not format ( ph -> ( Y ( 2nd ` K ) Z ) = ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) Z ) ) : No typesetting found for |- ( ph -> ( Y ( 2nd ` K ) Z ) = ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) Z ) ) with typecode |-
19	18	fveq1d	Could not format ( ph -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) Z ) ` H ) ) : No typesetting found for |- ( ph -> ( ( Y ( 2nd ` K ) Z ) ` H ) = ( ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) Z ) ` H ) ) with typecode |-
20		eqid	Could not format ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) : No typesetting found for |- ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) = ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) with typecode |-
21		eqidd	Could not format ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) ) : No typesetting found for |- ( ph -> ( F o.func ( C swapF D ) ) = ( F o.func ( C swapF D ) ) ) with typecode |-
22	3 4 5 21	cofuswapfcl	Could not format ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) ) : No typesetting found for |- ( ph -> ( F o.func ( C swapF D ) ) e. ( ( C Xc. D ) Func E ) ) with typecode |-
23		eqid	Could not format ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) : No typesetting found for |- ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) = ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) with typecode |-
24	20 2 3 4 22 8 6 23 9 10 11 12 13	curf12	Could not format ( ph -> ( ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) Z ) ` H ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , Z >. ) H ) ) : No typesetting found for |- ( ph -> ( ( Y ( 2nd ` ( ( 1st ` ( <. C , D >. curryF ( F o.func ( C swapF D ) ) ) ) ` X ) ) Z ) ` H ) = ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , Z >. ) H ) ) with typecode |-
25		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
26	2 25 11 3 6	catidcl	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)\in \left(X\mathrm{Hom}\left(C\right)X\right)$$
27	3 4 5 21 2 8 6 9 6 12 25 10 26 13	cofuswapf2	Could not format ( ph -> ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , Z >. ) H ) = ( H ( <. Y , X >. ( 2nd ` F ) <. Z , X >. ) ( .1. ` X ) ) ) : No typesetting found for |- ( ph -> ( ( .1. ` X ) ( <. X , Y >. ( 2nd ` ( F o.func ( C swapF D ) ) ) <. X , Z >. ) H ) = ( H ( <. Y , X >. ( 2nd ` F ) <. Z , X >. ) ( .1. ` X ) ) ) with typecode |-
28	19 24 27	3eqtrd	$$⊢\phi \to \left(Y{2}^{nd}\left(K\right)Z\right)\left(H\right)=H\left(⟨Y,X⟩2^{nd}\left(F\right)⟨Z,X⟩\right)\underset{\dot{}}{1}\left(X\right)$$