Definition df-cco

Description: Define the composition operation of a category. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	df-cco	⊢ comp = Slot ; 1 5

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cco	⊢ comp
1		c1	⊢ 1
2		c5	⊢ 5
3	1 2	cdc	⊢ ; 1 5
4	3	cslot	⊢ Slot ; 1 5
5	0 4	wceq	⊢ comp = Slot ; 1 5