Theorem fuconuniqvalslem

Description: Lemma for fuconuniqvals . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

	Ref	Expression
Hypotheses	fuconuniq2.c	$$⊢C=\mathrm{SetCat}\left(1_{𝑜}\right)$$
	fuconuniq2.e	$$⊢E=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}$$
	fuconuniq2.q	$$⊢Q=C\mathrm{FuncCat}E$$
	fuconuniq2.l	No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
	fuconuniq.a	$$⊢A=\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)$$
	fuconuniq.m	$$⊢M=\left(u\in 2_{𝑜},v\in 2_{𝑜}⟼\left(a\in \left(u\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)v\right)⟼A\left(a\right)\right)\right)$$
	fuconuniq.s	$$⊢S=⟨{\mathrm{I}\upharpoonright }_{2_{𝑜}},M⟩$$
	fuconuniq.r	$$⊢R=E\mathrm{FuncCat}E$$
	fuconuniq.o	No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) ) with typecode |-
	fuconuniq.k	No typesetting found for |- K = ( ( 1st ` .o. ) ` S ) with typecode |-
	fuconuniqvals.d	$$⊢D=E{\Delta }_{\mathrm{func}}C$$
	fuconuniqvals.f	$$⊢F=1^{st}\left(D\right)\left(\varnothing \right)$$
	fuconuniqvals.g	$$⊢G=1^{st}\left(D\right)\left(1_{𝑜}\right)$$
	fuconuniqvals.n	$$⊢N=1_{𝑜}\times \left\{\varnothing \right\}$$
	fuconuniqvalslem.t	$$⊢T=\left(C\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}C\right)$$
Assertion	fuconuniqvalslem	$$⊢\left(\left(N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)\right)\left(\varnothing \right)=\varnothing \wedge \left(N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)\right)\left(\varnothing \right)=1_{𝑜}\right)$$

Proof

Step	Hyp	Ref	Expression
1		fuconuniq2.c	$$⊢C=\mathrm{SetCat}\left(1_{𝑜}\right)$$
2		fuconuniq2.e	$$⊢E=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},2_{𝑜}⟩,⟨\mathrm{Hom}\left(\mathrm{ndx}\right),\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)⟩,⟨\mathrm{comp}\left(\mathrm{ndx}\right),\left(p\in \left(2_{𝑜}\times 2_{𝑜}\right),q\in 2_{𝑜}⟼\left(r\in 3_{𝑜},s\in 3_{𝑜}⟼r\cap s\right)\right)⟩\right\}$$
3		fuconuniq2.q	$$⊢Q=C\mathrm{FuncCat}E$$
4		fuconuniq2.l	Could not format L = ( <. C , C >. o.F E ) : No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
5		fuconuniq.a	$$⊢A=\left(b\in 3_{𝑜}⟼if\left(b=2_{𝑜},2_{𝑜},if\left(b=\varnothing ,1_{𝑜},\varnothing \right)\right)\right)$$
6		fuconuniq.m	$$⊢M=\left(u\in 2_{𝑜},v\in 2_{𝑜}⟼\left(a\in \left(u\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)v\right)⟼A\left(a\right)\right)\right)$$
7		fuconuniq.s	$$⊢S=⟨{\mathrm{I}\upharpoonright }_{2_{𝑜}},M⟩$$
8		fuconuniq.r	$$⊢R=E\mathrm{FuncCat}E$$
9		fuconuniq.o	Could not format .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) ) : No typesetting found for |- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) ) with typecode |-
10		fuconuniq.k	Could not format K = ( ( 1st ` .o. ) ` S ) : No typesetting found for |- K = ( ( 1st ` .o. ) ` S ) with typecode |-
11		fuconuniqvals.d	$$⊢D=E{\Delta }_{\mathrm{func}}C$$
12		fuconuniqvals.f	$$⊢F=1^{st}\left(D\right)\left(\varnothing \right)$$
13		fuconuniqvals.g	$$⊢G=1^{st}\left(D\right)\left(1_{𝑜}\right)$$
14		fuconuniqvals.n	$$⊢N=1_{𝑜}\times \left\{\varnothing \right\}$$
15		fuconuniqvalslem.t	$$⊢T=\left(C\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}C\right)$$
16	4	eqcomi	Could not format ( <. C , C >. o.F E ) = L : No typesetting found for |- ( <. C , C >. o.F E ) = L with typecode |-
17	16	fveq2i	Could not format ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) : No typesetting found for |- ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) with typecode |-
18	17	a1i	Could not format ( T. -> ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) ) : No typesetting found for |- ( T. -> ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) ) with typecode |-
19		eqid	$$⊢C\mathrm{FuncCat}C=C\mathrm{FuncCat}C$$
20		eqid	$$⊢\mathrm{Id}\left(C\mathrm{FuncCat}C\right)=\mathrm{Id}\left(C\mathrm{FuncCat}C\right)$$
21		eqid	$$⊢{id}_{\mathrm{func}}\left(C\right)={id}_{\mathrm{func}}\left(C\right)$$
22		setc1oterm	Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
23	1 22	eqeltri	Could not format C e. TermCat : No typesetting found for |- C e. TermCat with typecode |-
24	23	a1i	Could not format ( T. -> C e. TermCat ) : No typesetting found for |- ( T. -> C e. TermCat ) with typecode |-
25	24	termccatd	$$⊢\top \to C\in \mathrm{Cat}$$
26	1 2 11 12 13 14	par2diag	$$⊢\left(\left(F\in \left(C\mathrm{Func}E\right)\wedge G\in \left(C\mathrm{Func}E\right)\right)\wedge \left(N\in \left(F\left(C\mathrm{Nat}E\right)G\right)\wedge N\left(\varnothing \right)=\varnothing \right)\wedge \left(1^{st}\left(F\right)\left(\varnothing \right)=\varnothing \wedge 1^{st}\left(G\right)\left(\varnothing \right)=1_{𝑜}\right)\right)$$
27	26	simp2i	$$⊢\left(N\in \left(F\left(C\mathrm{Nat}E\right)G\right)\wedge N\left(\varnothing \right)=\varnothing \right)$$
28	27	simpli	$$⊢N\in \left(F\left(C\mathrm{Nat}E\right)G\right)$$
29	28	a1i	$$⊢\top \to N\in \left(F\left(C\mathrm{Nat}E\right)G\right)$$
30	18 19 20 21 25 29	fucoridid	$$⊢\top \to N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)=N$$
31	30	mptru	$$⊢N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)=N$$
32	31	fveq1i	$$⊢\left(N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)\right)\left(\varnothing \right)=N\left(\varnothing \right)$$
33	27	simpri	$$⊢N\left(\varnothing \right)=\varnothing$$
34	32 33	eqtri	$$⊢\left(N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)\right)\left(\varnothing \right)=\varnothing$$
35	2	par2catid	$$⊢\left(E\in \mathrm{Cat}\wedge \mathrm{Id}\left(E\right)=\left(y\in 2_{𝑜}⟼2_{𝑜}\right)\right)$$
36	35	simpli	$$⊢E\in \mathrm{Cat}$$
37	36	a1i	$$⊢\top \to E\in \mathrm{Cat}$$
38	2 5 6	parswapfunc	$$⊢⟨{\mathrm{I}\upharpoonright }_{2_{𝑜}},M⟩\in \left(E\mathrm{Func}E\right)$$
39	7 38	eqeltri	$$⊢S\in \left(E\mathrm{Func}E\right)$$
40	39	a1i	$$⊢\top \to S\in \left(E\mathrm{Func}E\right)$$
41		mptresid	$$⊢{\mathrm{I}\upharpoonright }_{2_{𝑜}}=\left(x\in 2_{𝑜}⟼x\right)$$
42		2oex	$$⊢2_{𝑜}\in \mathrm{V}$$
43	42	mptex	$$⊢\left(x\in 2_{𝑜}⟼x\right)\in \mathrm{V}$$
44	41 43	eqeltri	$$⊢{\mathrm{I}\upharpoonright }_{2_{𝑜}}\in \mathrm{V}$$
45	42 42	mpoex	$$⊢\left(u\in 2_{𝑜},v\in 2_{𝑜}⟼\left(a\in \left(u\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)v\right)⟼A\left(a\right)\right)\right)\in \mathrm{V}$$
46	6 45	eqeltri	$$⊢M\in \mathrm{V}$$
47	44 46	op1std	$$⊢S=⟨{\mathrm{I}\upharpoonright }_{2_{𝑜}},M⟩\to 1^{st}\left(S\right)={\mathrm{I}\upharpoonright }_{2_{𝑜}}$$
48	7 47	mp1i	$$⊢\top \to 1^{st}\left(S\right)={\mathrm{I}\upharpoonright }_{2_{𝑜}}$$
49	24 3 8 9 10 40 48	termcpostfix	$$⊢\top \to \left(K\in \left(Q\mathrm{Func}Q\right)\wedge 1^{st}\left(K\right)={\mathrm{I}\upharpoonright }_{\left(C\mathrm{Func}E\right)}\right)$$
50	49	simpld	$$⊢\top \to K\in \left(Q\mathrm{Func}Q\right)$$
51	26	simp1i	$$⊢\left(F\in \left(C\mathrm{Func}E\right)\wedge G\in \left(C\mathrm{Func}E\right)\right)$$
52	51	simpli	$$⊢F\in \left(C\mathrm{Func}E\right)$$
53	52	a1i	$$⊢\top \to F\in \left(C\mathrm{Func}E\right)$$
54	51	simpri	$$⊢G\in \left(C\mathrm{Func}E\right)$$
55	54	a1i	$$⊢\top \to G\in \left(C\mathrm{Func}E\right)$$
56	3 4 25 37 50 53 55 29 21 20	fucoaltval	$$⊢\top \to N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)=\left(F{2}^{nd}\left(K\right)G\right)\left(N\right)$$
57	56	mptru	$$⊢N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)=\left(F{2}^{nd}\left(K\right)G\right)\left(N\right)$$
58	57	fveq1i	$$⊢\left(N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)\right)\left(\varnothing \right)=\left(F{2}^{nd}\left(K\right)G\right)\left(N\right)\left(\varnothing \right)$$
59		0lt1o	$$⊢\varnothing \in 1_{𝑜}$$
60	1	setc1obas	$$⊢1_{𝑜}={\mathrm{Base}}_C$$
61	59 60	eleqtri	$$⊢\varnothing \in {\mathrm{Base}}_C$$
62	61	a1i	$$⊢\top \to \varnothing \in {\mathrm{Base}}_C$$
63	3 8 9 40 25 10 53 55 29 62	postcof2	$$⊢\top \to \left(F{2}^{nd}\left(K\right)G\right)\left(N\right)\left(\varnothing \right)=\left(1^{st}\left(F\right)\left(\varnothing \right)2^{nd}\left(S\right)1^{st}\left(G\right)\left(\varnothing \right)\right)\left(N\left(\varnothing \right)\right)$$
64	63	mptru	$$⊢\left(F{2}^{nd}\left(K\right)G\right)\left(N\right)\left(\varnothing \right)=\left(1^{st}\left(F\right)\left(\varnothing \right)2^{nd}\left(S\right)1^{st}\left(G\right)\left(\varnothing \right)\right)\left(N\left(\varnothing \right)\right)$$
65	26	simp3i	$$⊢\left(1^{st}\left(F\right)\left(\varnothing \right)=\varnothing \wedge 1^{st}\left(G\right)\left(\varnothing \right)=1_{𝑜}\right)$$
66	65	simpli	$$⊢1^{st}\left(F\right)\left(\varnothing \right)=\varnothing$$
67	65	simpri	$$⊢1^{st}\left(G\right)\left(\varnothing \right)=1_{𝑜}$$
68	44 46	op2ndd	$$⊢S=⟨{\mathrm{I}\upharpoonright }_{2_{𝑜}},M⟩\to 2^{nd}\left(S\right)=M$$
69	7 68	ax-mp	$$⊢2^{nd}\left(S\right)=M$$
70	66 67 69	oveq123i	$$⊢1^{st}\left(F\right)\left(\varnothing \right)2^{nd}\left(S\right)1^{st}\left(G\right)\left(\varnothing \right)=\varnothing M{1}_{𝑜}$$
71	70 33	fveq12i	$$⊢\left(1^{st}\left(F\right)\left(\varnothing \right)2^{nd}\left(S\right)1^{st}\left(G\right)\left(\varnothing \right)\right)\left(N\left(\varnothing \right)\right)=\left(\varnothing M{1}_{𝑜}\right)\left(\varnothing \right)$$
72	64 71	eqtri	$$⊢\left(F{2}^{nd}\left(K\right)G\right)\left(N\right)\left(\varnothing \right)=\left(\varnothing M{1}_{𝑜}\right)\left(\varnothing \right)$$
73		0ex	$$⊢\varnothing \in \mathrm{V}$$
74	73	prid1	$$⊢\varnothing \in \left\{\varnothing ,1_{𝑜}\right\}$$
75		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
76	74 75	eleqtrri	$$⊢\varnothing \in 2_{𝑜}$$
77	76	a1i	$$⊢\top \to \varnothing \in 2_{𝑜}$$
78		1oelpr	$$⊢1_{𝑜}\in \left\{\varnothing ,1_{𝑜}\right\}$$
79	78 75	eleqtrri	$$⊢1_{𝑜}\in 2_{𝑜}$$
80	79	a1i	$$⊢\top \to 1_{𝑜}\in 2_{𝑜}$$
81		eqid	$$⊢\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)=\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)$$
82	81	par2hom	$$⊢\left(\varnothing \left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)\varnothing =\left\{2_{𝑜}\right\}\wedge 1_{𝑜}\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)1_{𝑜}=\left\{2_{𝑜}\right\}\wedge \left(\varnothing \left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)1_{𝑜}=2_{𝑜}\wedge 1_{𝑜}\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)\varnothing =\varnothing \right)\right)$$
83	82	simp3i	$$⊢\left(\varnothing \left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)1_{𝑜}=2_{𝑜}\wedge 1_{𝑜}\left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)\varnothing =\varnothing \right)$$
84	83	simpli	$$⊢\varnothing \left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)1_{𝑜}=2_{𝑜}$$
85	76 84	eleqtrri	$$⊢\varnothing \in \left(\varnothing \left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)1_{𝑜}\right)$$
86	85	a1i	$$⊢\top \to \varnothing \in \left(\varnothing \left(m\in 2_{𝑜},n\in 2_{𝑜}⟼if\left(m=n,\left\{2_{𝑜}\right\},if\left(\left(m=\varnothing \wedge n=1_{𝑜}\right),2_{𝑜},\varnothing \right)\right)\right)1_{𝑜}\right)$$
87	6 77 80 86	fvmpomptd	$$⊢\top \to \left(\varnothing M{1}_{𝑜}\right)\left(\varnothing \right)=A\left(\varnothing \right)$$
88	87	mptru	$$⊢\left(\varnothing M{1}_{𝑜}\right)\left(\varnothing \right)=A\left(\varnothing \right)$$
89	5	parswapprop	$$⊢\left(A\left(2_{𝑜}\right)=2_{𝑜}\wedge \forall t\in 2_{𝑜}A\left(t\right)\in 2_{𝑜}\wedge A\left(\varnothing \right)=1_{𝑜}\right)$$
90	89	simp3i	$$⊢A\left(\varnothing \right)=1_{𝑜}$$
91	72 88 90	3eqtri	$$⊢\left(F{2}^{nd}\left(K\right)G\right)\left(N\right)\left(\varnothing \right)=1_{𝑜}$$
92	58 91	eqtri	$$⊢\left(N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)\right)\left(\varnothing \right)=1_{𝑜}$$
93	34 92	pm3.2i	$$⊢\left(\left(N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)\right)\left(\varnothing \right)=\varnothing \wedge \left(N\left(⟨F,{id}_{\mathrm{func}}\left(C\right)⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,{id}_{\mathrm{func}}\left(C\right)⟩\right)\mathrm{Id}\left(C\mathrm{FuncCat}C\right)\left({id}_{\mathrm{func}}\left(C\right)\right)\right)\left(\varnothing \right)=1_{𝑜}\right)$$