Theorem fuconuniqvals

Description: At the same natural-transformation/identity input, the canonical and alternative morphism maps give respectively (/) and 1o at the unique source object (/) . (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	fuconuniq2.c	|- C = ( SetCat ` 1o )
	fuconuniq2.e	|- E = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. }
	fuconuniq2.q	|- Q = ( C FuncCat E )
	fuconuniq2.l	|- L = ( <. C , C >. o.F E )
	fuconuniq.a	|- A = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
	fuconuniq.m	|- M = ( u e. 2o , v e. 2o |-> ( a e. ( u ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) v ) |-> ( A ` a ) ) )
	fuconuniq.s	|- S = <. ( _I |` 2o ) , M >.
	fuconuniq.r	|- R = ( E FuncCat E )
	fuconuniq.o	|- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) )
	fuconuniq.k	|- K = ( ( 1st ` .o. ) ` S )
	fuconuniqvals.d	|- D = ( E DiagFunc C )
	fuconuniqvals.f	|- F = ( ( 1st ` D ) ` (/) )
	fuconuniqvals.g	|- G = ( ( 1st ` D ) ` 1o )
	fuconuniqvals.n	|- N = ( 1o X. { (/) } )
Assertion	fuconuniqvals	|- ( ( ( N ( <. F , ( idFunc ` C ) >. ( 2nd ` L ) <. G , ( idFunc ` C ) >. ) ( ( Id ` ( C FuncCat C ) ) ` ( idFunc ` C ) ) ) ` (/) ) = (/) /\ ( ( N ( <. F , ( idFunc ` C ) >. ( 2nd ` ( K o.func L ) ) <. G , ( idFunc ` C ) >. ) ( ( Id ` ( C FuncCat C ) ) ` ( idFunc ` C ) ) ) ` (/) ) = 1o )

Proof

Step	Hyp	Ref	Expression
1		fuconuniq2.c	|- C = ( SetCat ` 1o )
2		fuconuniq2.e	|- E = { <. ( Base ` ndx ) , 2o >. , <. ( Hom ` ndx ) , ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) >. , <. ( comp ` ndx ) , ( p e. ( 2o X. 2o ) , q e. 2o |-> ( r e. 3o , s e. 3o |-> ( r i^i s ) ) ) >. }
3		fuconuniq2.q	|- Q = ( C FuncCat E )
4		fuconuniq2.l	|- L = ( <. C , C >. o.F E )
5		fuconuniq.a	|- A = ( b e. 3o |-> if ( b = 2o , 2o , if ( b = (/) , 1o , (/) ) ) )
6		fuconuniq.m	|- M = ( u e. 2o , v e. 2o |-> ( a e. ( u ( m e. 2o , n e. 2o |-> if ( m = n , { 2o } , if ( ( m = (/) /\ n = 1o ) , 2o , (/) ) ) ) v ) |-> ( A ` a ) ) )
7		fuconuniq.s	|- S = <. ( _I |` 2o ) , M >.
8		fuconuniq.r	|- R = ( E FuncCat E )
9		fuconuniq.o	|- .o. = ( <. R , Q >. curryF ( <. C , E >. o.F E ) )
10		fuconuniq.k	|- K = ( ( 1st ` .o. ) ` S )
11		fuconuniqvals.d	|- D = ( E DiagFunc C )
12		fuconuniqvals.f	|- F = ( ( 1st ` D ) ` (/) )
13		fuconuniqvals.g	|- G = ( ( 1st ` D ) ` 1o )
14		fuconuniqvals.n	|- N = ( 1o X. { (/) } )
15		eqid	|- ( ( C FuncCat E ) Xc. ( C FuncCat C ) ) = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
16	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	fuconuniqvalslem	|- ( ( ( N ( <. F , ( idFunc ` C ) >. ( 2nd ` L ) <. G , ( idFunc ` C ) >. ) ( ( Id ` ( C FuncCat C ) ) ` ( idFunc ` C ) ) ) ` (/) ) = (/) /\ ( ( N ( <. F , ( idFunc ` C ) >. ( 2nd ` ( K o.func L ) ) <. G , ( idFunc ` C ) >. ) ( ( Id ` ( C FuncCat C ) ) ` ( idFunc ` C ) ) ) ` (/) ) = 1o )