Theorem cmddu

Description: The duality of limits and colimits: colimits of a diagram are limits of an opposite diagram in opposite categories. (Contributed by Zhi Wang, 20-Nov-2025)

	Ref	Expression
Hypotheses	lmddu.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	lmddu.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	lmddu.g	No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
	lmddu.c	$$⊢\phi \to C\in V$$
	lmddu.d	$$⊢\phi \to D\in W$$
Assertion	cmddu	Could not format assertion : No typesetting found for |- ( ph -> ( ( C Colimit D ) ` F ) = ( ( O Limit P ) ` G ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		lmddu.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		lmddu.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		lmddu.g	Could not format G = ( oppFunc ` F ) : No typesetting found for |- G = ( oppFunc ` F ) with typecode |-
4		lmddu.c	$$⊢\phi \to C\in V$$
5		lmddu.d	$$⊢\phi \to D\in W$$
6		relup	Could not format Rel ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) : No typesetting found for |- Rel ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) with typecode |-
7		relup	Could not format Rel ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) : No typesetting found for |- Rel ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) with typecode |-
8		simpr	Could not format ( ( ph /\ x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) -> x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) : No typesetting found for |- ( ( ph /\ x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) -> x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) with typecode |-
9	8	up1st2nd	Could not format ( ( ph /\ x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) -> x ( <. ( 1st ` ( C DiagFunc D ) ) , ( 2nd ` ( C DiagFunc D ) ) >. ( C UP ( D FuncCat C ) ) F ) m ) : No typesetting found for |- ( ( ph /\ x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) -> x ( <. ( 1st ` ( C DiagFunc D ) ) , ( 2nd ` ( C DiagFunc D ) ) >. ( C UP ( D FuncCat C ) ) F ) m ) with typecode |-
10		eqid	$$⊢D\mathrm{FuncCat}C=D\mathrm{FuncCat}C$$
11	10	fucbas	$$⊢D\mathrm{Func}C={\mathrm{Base}}_{\left(D\mathrm{FuncCat}C\right)}$$
12	9 11	uprcl3	Could not format ( ( ph /\ x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) -> F e. ( D Func C ) ) : No typesetting found for |- ( ( ph /\ x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m ) -> F e. ( D Func C ) ) with typecode |-
13	5	adantr	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> D e. W ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> D e. W ) with typecode |-
14	4	adantr	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> C e. V ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> C e. V ) with typecode |-
15		eqid	$$⊢\mathrm{oppCat}\left(P\right)=\mathrm{oppCat}\left(P\right)$$
16		eqid	$$⊢\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(O\right)$$
17	2	fvexi	$$⊢P\in \mathrm{V}$$
18	17	a1i	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> P e. _V ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> P e. _V ) with typecode |-
19	1	fvexi	$$⊢O\in \mathrm{V}$$
20	19	a1i	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> O e. _V ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> O e. _V ) with typecode |-
21		simpr	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) with typecode |-
22	21	up1st2nd	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> x ( <. ( 1st ` ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ) , ( 2nd ` ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ) >. ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> x ( <. ( 1st ` ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ) , ( 2nd ` ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ) >. ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) with typecode |-
23		eqid	$$⊢\mathrm{oppCat}\left(P\right)\mathrm{FuncCat}\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(P\right)\mathrm{FuncCat}\mathrm{oppCat}\left(O\right)$$
24	23	fucbas	$$⊢\mathrm{oppCat}\left(P\right)\mathrm{Func}\mathrm{oppCat}\left(O\right)={\mathrm{Base}}_{\left(\mathrm{oppCat}\left(P\right)\mathrm{FuncCat}\mathrm{oppCat}\left(O\right)\right)}$$
25	22 24	uprcl3	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> ( oppFunc ` G ) e. ( ( oppCat ` P ) Func ( oppCat ` O ) ) ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> ( oppFunc ` G ) e. ( ( oppCat ` P ) Func ( oppCat ` O ) ) ) with typecode |-
26	15 16 18 20 25	funcoppc5	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> G e. ( P Func O ) ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> G e. ( P Func O ) ) with typecode |-
27	3 26	eqeltrrid	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> ( oppFunc ` F ) e. ( P Func O ) ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> ( oppFunc ` F ) e. ( P Func O ) ) with typecode |-
28	2 1 13 14 27	funcoppc5	Could not format ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> F e. ( D Func C ) ) : No typesetting found for |- ( ( ph /\ x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) -> F e. ( D Func C ) ) with typecode |-
29	1	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
30	29	a1i	$$⊢F\in \left(D\mathrm{Func}C\right)\to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
31	1	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
32	31	a1i	$$⊢F\in \left(D\mathrm{Func}C\right)\to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
33	2	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\right)$$
34	33	a1i	$$⊢F\in \left(D\mathrm{Func}C\right)\to {\mathrm{Hom}}_{𝑓}\left(D\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\right)$$
35	2	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\right)$$
36	35	a1i	$$⊢F\in \left(D\mathrm{Func}C\right)\to {\mathrm{comp}}_{𝑓}\left(D\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\right)$$
37		funcrcl	$$⊢F\in \left(D\mathrm{Func}C\right)\to \left(D\in \mathrm{Cat}\wedge C\in \mathrm{Cat}\right)$$
38	37	simpld	$$⊢F\in \left(D\mathrm{Func}C\right)\to D\in \mathrm{Cat}$$
39	2	oppccat	$$⊢D\in \mathrm{Cat}\to P\in \mathrm{Cat}$$
40	15	oppccat	$$⊢P\in \mathrm{Cat}\to \mathrm{oppCat}\left(P\right)\in \mathrm{Cat}$$
41	38 39 40	3syl	$$⊢F\in \left(D\mathrm{Func}C\right)\to \mathrm{oppCat}\left(P\right)\in \mathrm{Cat}$$
42	37	simprd	$$⊢F\in \left(D\mathrm{Func}C\right)\to C\in \mathrm{Cat}$$
43	1	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
44	16	oppccat	$$⊢O\in \mathrm{Cat}\to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
45	42 43 44	3syl	$$⊢F\in \left(D\mathrm{Func}C\right)\to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
46	34 36 30 32 38 41 42 45	fucpropd	$$⊢F\in \left(D\mathrm{Func}C\right)\to D\mathrm{FuncCat}C=\mathrm{oppCat}\left(P\right)\mathrm{FuncCat}\mathrm{oppCat}\left(O\right)$$
47	46	fveq2d	$$⊢F\in \left(D\mathrm{Func}C\right)\to {\mathrm{Hom}}_{𝑓}\left(D\mathrm{FuncCat}C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\mathrm{FuncCat}\mathrm{oppCat}\left(O\right)\right)$$
48	46	fveq2d	$$⊢F\in \left(D\mathrm{Func}C\right)\to {\mathrm{comp}}_{𝑓}\left(D\mathrm{FuncCat}C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(P\right)\mathrm{FuncCat}\mathrm{oppCat}\left(O\right)\right)$$
49	10 38 42	fuccat	$$⊢F\in \left(D\mathrm{Func}C\right)\to D\mathrm{FuncCat}C\in \mathrm{Cat}$$
50	46 49	eqeltrrd	$$⊢F\in \left(D\mathrm{Func}C\right)\to \mathrm{oppCat}\left(P\right)\mathrm{FuncCat}\mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
51	30 32 47 48 42 45 49 50	uppropd	Could not format ( F e. ( D Func C ) -> ( C UP ( D FuncCat C ) ) = ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ) : No typesetting found for |- ( F e. ( D Func C ) -> ( C UP ( D FuncCat C ) ) = ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ) with typecode |-
52	30 32 34 36 42 45 38 41	diagpropd	$$⊢F\in \left(D\mathrm{Func}C\right)\to C{\Delta }_{\mathrm{func}}D=\mathrm{oppCat}\left(O\right){\Delta }_{\mathrm{func}}\mathrm{oppCat}\left(P\right)$$
53		id	$$⊢F\in \left(D\mathrm{Func}C\right)\to F\in \left(D\mathrm{Func}C\right)$$
54	2 1 53	oppfoppc2	Could not format ( F e. ( D Func C ) -> ( oppFunc ` F ) e. ( P Func O ) ) : No typesetting found for |- ( F e. ( D Func C ) -> ( oppFunc ` F ) e. ( P Func O ) ) with typecode |-
55	3 54	eqeltrid	$$⊢F\in \left(D\mathrm{Func}C\right)\to G\in \left(P\mathrm{Func}O\right)$$
56		relfunc	$$⊢\mathrm{Rel}\left(P\mathrm{Func}O\right)$$
57	55 56 3	2oppf	Could not format ( F e. ( D Func C ) -> ( oppFunc ` G ) = F ) : No typesetting found for |- ( F e. ( D Func C ) -> ( oppFunc ` G ) = F ) with typecode |-
58	57	eqcomd	Could not format ( F e. ( D Func C ) -> F = ( oppFunc ` G ) ) : No typesetting found for |- ( F e. ( D Func C ) -> F = ( oppFunc ` G ) ) with typecode |-
59	51 52 58	oveq123d	Could not format ( F e. ( D Func C ) -> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) = ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) ) : No typesetting found for |- ( F e. ( D Func C ) -> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) = ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) ) with typecode |-
60	59	breqd	Could not format ( F e. ( D Func C ) -> ( x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m <-> x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) ) : No typesetting found for |- ( F e. ( D Func C ) -> ( x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m <-> x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) ) with typecode |-
61	12 28 60	pm5.21nd	Could not format ( ph -> ( x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m <-> x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) ) : No typesetting found for |- ( ph -> ( x ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) m <-> x ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) m ) ) with typecode |-
62	6 7 61	eqbrrdiv	Could not format ( ph -> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) = ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) ) : No typesetting found for |- ( ph -> ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) = ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) ) with typecode |-
63		cmdfval2	Could not format ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) : No typesetting found for |- ( ( C Colimit D ) ` F ) = ( ( C DiagFunc D ) ( C UP ( D FuncCat C ) ) F ) with typecode |-
64		cmdfval2	Could not format ( ( ( oppCat ` O ) Colimit ( oppCat ` P ) ) ` ( oppFunc ` G ) ) = ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) : No typesetting found for |- ( ( ( oppCat ` O ) Colimit ( oppCat ` P ) ) ` ( oppFunc ` G ) ) = ( ( ( oppCat ` O ) DiagFunc ( oppCat ` P ) ) ( ( oppCat ` O ) UP ( ( oppCat ` P ) FuncCat ( oppCat ` O ) ) ) ( oppFunc ` G ) ) with typecode |-
65	62 63 64	3eqtr4g	Could not format ( ph -> ( ( C Colimit D ) ` F ) = ( ( ( oppCat ` O ) Colimit ( oppCat ` P ) ) ` ( oppFunc ` G ) ) ) : No typesetting found for |- ( ph -> ( ( C Colimit D ) ` F ) = ( ( ( oppCat ` O ) Colimit ( oppCat ` P ) ) ` ( oppFunc ` G ) ) ) with typecode |-
66		eqid	Could not format ( oppFunc ` G ) = ( oppFunc ` G ) : No typesetting found for |- ( oppFunc ` G ) = ( oppFunc ` G ) with typecode |-
67	19	a1i	$$⊢\phi \to O\in \mathrm{V}$$
68	17	a1i	$$⊢\phi \to P\in \mathrm{V}$$
69	16 15 66 67 68	lmddu	Could not format ( ph -> ( ( O Limit P ) ` G ) = ( ( ( oppCat ` O ) Colimit ( oppCat ` P ) ) ` ( oppFunc ` G ) ) ) : No typesetting found for |- ( ph -> ( ( O Limit P ) ` G ) = ( ( ( oppCat ` O ) Colimit ( oppCat ` P ) ) ` ( oppFunc ` G ) ) ) with typecode |-
70	65 69	eqtr4d	Could not format ( ph -> ( ( C Colimit D ) ` F ) = ( ( O Limit P ) ` G ) ) : No typesetting found for |- ( ph -> ( ( C Colimit D ) ` F ) = ( ( O Limit P ) ` G ) ) with typecode |-