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	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	diagffth.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
	diagffth.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
	diagciso.e	⊢ 𝐸 = ( CatCat ‘ 𝑈 )
	diagciso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	diagciso.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
	diagciso.1	⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
	diagciso.i	⊢ 𝐼 = ( Iso ‘ 𝐸 )
	diagciso.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
Assertion	diagciso	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 𝐼 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		diagffth.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		diagffth.d	⊢ ( 𝜑 → 𝐷 ∈ TermCat )
3		diagffth.q	⊢ 𝑄 = ( 𝐷 FuncCat 𝐶 )
4		diagciso.e	⊢ 𝐸 = ( CatCat ‘ 𝑈 )
5		diagciso.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
6		diagciso.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑈 )
7		diagciso.1	⊢ ( 𝜑 → 𝑄 ∈ 𝑈 )
8		diagciso.i	⊢ 𝐼 = ( Iso ‘ 𝐸 )
9		diagciso.l	⊢ 𝐿 = ( 𝐶 Δfunc 𝐷 )
10	1 2 3 9	diagffth	⊢ ( 𝜑 → 𝐿 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) )
11		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
12	11 2 1 9	diag1f1o	⊢ ( 𝜑 → ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 𝐷 Func 𝐶 ) )
13		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
14	3	fucbas	⊢ ( 𝐷 Func 𝐶 ) = ( Base ‘ 𝑄 )
15	6 1	elind	⊢ ( 𝜑 → 𝐶 ∈ ( 𝑈 ∩ Cat ) )
16	4 13 5	catcbas	⊢ ( 𝜑 → ( Base ‘ 𝐸 ) = ( 𝑈 ∩ Cat ) )
17	15 16	eleqtrrd	⊢ ( 𝜑 → 𝐶 ∈ ( Base ‘ 𝐸 ) )
18	2	termccatd	⊢ ( 𝜑 → 𝐷 ∈ Cat )
19	3 18 1	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
20	7 19	elind	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑈 ∩ Cat ) )
21	20 16	eleqtrrd	⊢ ( 𝜑 → 𝑄 ∈ ( Base ‘ 𝐸 ) )
22	4 13 11 14 5 17 21 8	catciso	⊢ ( 𝜑 → ( 𝐿 ∈ ( 𝐶 𝐼 𝑄 ) ↔ ( 𝐿 ∈ ( ( 𝐶 Full 𝑄 ) ∩ ( 𝐶 Faith 𝑄 ) ) ∧ ( 1st ‘ 𝐿 ) : ( Base ‘ 𝐶 ) –1-1-onto→ ( 𝐷 Func 𝐶 ) ) ) )
23	10 12 22	mpbir2and	⊢ ( 𝜑 → 𝐿 ∈ ( 𝐶 𝐼 𝑄 ) )