diagcl

Description: The diagonal functor is a functor from the base category to the functor category. Another way of saying this is that the constant functor ( y e. D |-> X ) is a construction that is natural in X (and covariant). (Contributed by Mario Carneiro, 7-Jan-2017) (Revised by Mario Carneiro, 15-Jan-2017)

	Ref	Expression
Hypotheses	diagval.l	$⊢ L = C Δ_{func} D$
	diagval.c	$⊢ φ \to C \in Cat$
	diagval.d	$⊢ φ \to D \in Cat$
	diagcl.q	$⊢ Q = D FuncCat C$
Assertion	diagcl	$⊢ φ \to L \in (C Func Q)$

Proof

Step	Hyp	Ref	Expression
1		diagval.l	$⊢ L = C Δ_{func} D$
2		diagval.c	$⊢ φ \to C \in Cat$
3		diagval.d	$⊢ φ \to D \in Cat$
4		diagcl.q	$⊢ Q = D FuncCat C$
5	1 2 3	diagval	$⊢ φ \to L = ⟨C, D⟩ {curry}_{F} (C {1^{st}}_{F} D)$
6		eqid	$⊢ ⟨C, D⟩ {curry}_{F} (C {1^{st}}_{F} D) = ⟨C, D⟩ {curry}_{F} (C {1^{st}}_{F} D)$
7		eqid	$⊢ C \times_{c} D = C \times_{c} D$
8		eqid	$⊢ C {1^{st}}_{F} D = C {1^{st}}_{F} D$
9	7 2 3 8	1stfcl	$⊢ φ \to C {1^{st}}_{F} D \in ((C \times_{c} D) Func C)$
10	6 4 2 3 9	curfcl	$⊢ φ \to ⟨C, D⟩ {curry}_{F} (C {1^{st}}_{F} D) \in (C Func Q)$
11	5 10	eqeltrd	$⊢ φ \to L \in (C Func Q)$

Metamath Proof Explorer

Theorem diagcl

Proof