Theorem diagciso

Description: The diagonal functor is an isomorphism from a category C to the category of functors from a terminal category to C .

It is provable that the inverse of the diagonal functor is the mapped object by the transposed curry of ( D evalF C ) , i.e., U. ran ( 1st( <. D , Q >. curryF ( ( D evalF C ) o.func ( D swapF Q ) ) ) ) .

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

	Ref	Expression
Hypotheses	diagffth.c	|- ( ph -> C e. Cat )
	diagffth.d	|- ( ph -> D e. TermCat )
	diagffth.q	|- Q = ( D FuncCat C )
	diagciso.e	|- E = ( CatCat ` U )
	diagciso.u	|- ( ph -> U e. V )
	diagciso.c	|- ( ph -> C e. U )
	diagciso.1	|- ( ph -> Q e. U )
	diagciso.i	|- I = ( Iso ` E )
	diagciso.l	|- L = ( C DiagFunc D )
Assertion	diagciso	|- ( ph -> L e. ( C I Q ) )

Proof

Step	Hyp	Ref	Expression
1		diagffth.c	|- ( ph -> C e. Cat )
2		diagffth.d	|- ( ph -> D e. TermCat )
3		diagffth.q	|- Q = ( D FuncCat C )
4		diagciso.e	|- E = ( CatCat ` U )
5		diagciso.u	|- ( ph -> U e. V )
6		diagciso.c	|- ( ph -> C e. U )
7		diagciso.1	|- ( ph -> Q e. U )
8		diagciso.i	|- I = ( Iso ` E )
9		diagciso.l	|- L = ( C DiagFunc D )
10	1 2 3 9	diagffth	|- ( ph -> L e. ( ( C Full Q ) i^i ( C Faith Q ) ) )
11		eqid	|- ( Base ` C ) = ( Base ` C )
12	11 2 1 9	diag1f1o	|- ( ph -> ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( D Func C ) )
13		eqid	|- ( Base ` E ) = ( Base ` E )
14	3	fucbas	|- ( D Func C ) = ( Base ` Q )
15	6 1	elind	|- ( ph -> C e. ( U i^i Cat ) )
16	4 13 5	catcbas	|- ( ph -> ( Base ` E ) = ( U i^i Cat ) )
17	15 16	eleqtrrd	|- ( ph -> C e. ( Base ` E ) )
18	2	termccd	|- ( ph -> D e. Cat )
19	3 18 1	fuccat	|- ( ph -> Q e. Cat )
20	7 19	elind	|- ( ph -> Q e. ( U i^i Cat ) )
21	20 16	eleqtrrd	|- ( ph -> Q e. ( Base ` E ) )
22	4 13 11 14 5 17 21 8	catciso	|- ( ph -> ( L e. ( C I Q ) <-> ( L e. ( ( C Full Q ) i^i ( C Faith Q ) ) /\ ( 1st ` L ) : ( Base ` C ) -1-1-onto-> ( D Func C ) ) ) )
23	10 12 22	mpbir2and	|- ( ph -> L e. ( C I Q ) )