fucoaltval

Description: At a pair consisting of a natural transformation and the identity of the identity functor, post-composed functor composition acts by the post- composing functor on that natural transformation. (Contributed by Zhi Wang, 14-Sep-2026) (Revised by Zhi Wang, 17-Sep-2026)

	Ref	Expression
Hypotheses	fucoaltfunc.q	$⊢ Q = C FuncCat E$
	fucoaltval.l	No typesetting found for \|- L = ( <. C , C >. o.F E ) with typecode \|-
	fucoaltval.c	$⊢ φ \to C \in Cat$
	fucoaltval.e	$⊢ φ \to E \in Cat$
	fucoaltval.k	$⊢ φ \to K \in (Q Func Q)$
	fucoaltval.f	$⊢ φ \to F \in (C Func E)$
	fucoaltval.g	$⊢ φ \to G \in (C Func E)$
	fucoaltval.a	$⊢ φ \to A \in (F (C Nat E) G)$
	fucoaltval.i	$⊢ I = {id}_{func} (C)$
	fucoaltval.j	$⊢ J = Id (C FuncCat C)$
Assertion	fucoaltval	$⊢ φ \to A (⟨F, I⟩ 2^{nd} (K \circ_{func} L) ⟨G, I⟩) J (I) = (F 2^{nd} (K) G) (A)$

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	$⊢ Q = C FuncCat E$
2		fucoaltval.l	Could not format L = ( <. C , C >. o.F E ) : No typesetting found for \|- L = ( <. C , C >. o.F E ) with typecode \|-
3		fucoaltval.c	$⊢ φ \to C \in Cat$
4		fucoaltval.e	$⊢ φ \to E \in Cat$
5		fucoaltval.k	$⊢ φ \to K \in (Q Func Q)$
6		fucoaltval.f	$⊢ φ \to F \in (C Func E)$
7		fucoaltval.g	$⊢ φ \to G \in (C Func E)$
8		fucoaltval.a	$⊢ φ \to A \in (F (C Nat E) G)$
9		fucoaltval.i	$⊢ I = {id}_{func} (C)$
10		fucoaltval.j	$⊢ J = Id (C FuncCat C)$
11		eqid	$⊢ (C FuncCat E) \times_{c} (C FuncCat C) = (C FuncCat E) \times_{c} (C FuncCat C)$
12	1 2 3 4 5 6 7 8 9 10 11	fucoaltvallem	$⊢ φ \to A (⟨F, I⟩ 2^{nd} (K \circ_{func} L) ⟨G, I⟩) J (I) = (F 2^{nd} (K) G) (A)$

Metamath Proof Explorer

Theorem fucoaltval

Proof