Theorem diag1a

Description: The constant functor of X . (Contributed by Zhi Wang, 19-Oct-2025)

	Ref	Expression
Hypotheses	diag1.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
	diag1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	diag1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
	diag1.a	$$⊢A={\mathrm{Base}}_C$$
	diag1.x	$$⊢\phi \to X\in A$$
	diag1.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
	diag1.b	$$⊢B={\mathrm{Base}}_D$$
	diag1.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
	diag1.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
Assertion	diag1a	$$⊢\phi \to K=⟨B\times \left\{X\right\},\left(y\in B,z\in B⟼\left(yJz\right)\times \left\{\underset{\dot{}}{1}\left(X\right)\right\}\right)⟩$$

Proof

Step	Hyp	Ref	Expression
1		diag1.l	$$⊢L=C{\Delta }_{\mathrm{func}}D$$
2		diag1.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		diag1.d	$$⊢\phi \to D\in \mathrm{Cat}$$
4		diag1.a	$$⊢A={\mathrm{Base}}_C$$
5		diag1.x	$$⊢\phi \to X\in A$$
6		diag1.k	$$⊢K=1^{st}\left(L\right)\left(X\right)$$
7		diag1.b	$$⊢B={\mathrm{Base}}_D$$
8		diag1.j	$$⊢J=\mathrm{Hom}\left(D\right)$$
9		diag1.i	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
10	1 2 3 4 5 6 7 8 9	diag1	$$⊢\phi \to K=⟨\left(y\in B⟼X\right),\left(y\in B,z\in B⟼\left(f\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(X\right)\right)\right)⟩$$
11		fconstmpt	$$⊢B\times \left\{X\right\}=\left(y\in B⟼X\right)$$
12		fconstmpt	$$⊢\left(yJz\right)\times \left\{\underset{\dot{}}{1}\left(X\right)\right\}=\left(f\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(X\right)\right)$$
13	12	a1i	$$⊢\left(y\in B\wedge z\in B\right)\to \left(yJz\right)\times \left\{\underset{\dot{}}{1}\left(X\right)\right\}=\left(f\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(X\right)\right)$$
14	13	mpoeq3ia	$$⊢\left(y\in B,z\in B⟼\left(yJz\right)\times \left\{\underset{\dot{}}{1}\left(X\right)\right\}\right)=\left(y\in B,z\in B⟼\left(f\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(X\right)\right)\right)$$
15	11 14	opeq12i	$$⊢⟨B\times \left\{X\right\},\left(y\in B,z\in B⟼\left(yJz\right)\times \left\{\underset{\dot{}}{1}\left(X\right)\right\}\right)⟩=⟨\left(y\in B⟼X\right),\left(y\in B,z\in B⟼\left(f\in \left(yJz\right)⟼\underset{\dot{}}{1}\left(X\right)\right)\right)⟩$$
16	10 15	eqtr4di	$$⊢\phi \to K=⟨B\times \left\{X\right\},\left(y\in B,z\in B⟼\left(yJz\right)\times \left\{\underset{\dot{}}{1}\left(X\right)\right\}\right)⟩$$