- intro;
- constructor 1;
- [ @(objs1 c);
- | intros; @(setoid2_of_setoid1 (arrows1 c o o1));
- | @(id1 c);
- | intros;
- constructor 1;
- [ intros; @(comp1 c o1 o2 o3 c1 c2);
- | intros; unfold setoid2_of_setoid1 in e e1 a a' b b'; simplify in e e1 a a' b b';
- change with ((b∘a) =_1 (b'∘a')); @(e‡e1); ]
- | intros; simplify; whd in a12 a23 a34; whd; @rule (ASSOC);
- | intros; simplify; whd in a; whd; @id_neutral_right1;
- | intros; simplify; whd in a; whd; @id_neutral_left1; ]
+ #c
+ @mk_category2
+ [ @(objs1 c)
+ | #o #o1 @(setoid2_of_setoid1 (arrows1 c o o1))
+ | @(id1 c)
+ | #o1 #o2 #o3
+ @mk_binary_morphism2
+ [ #c1 #c2 @(comp1 c o1 o2 o3 c1 c2)
+ | #a #a' #b #b' #e #e1 @(e‡e1) ]
+ | #o1 #o2 #o3 #o4 #a12 #a23 #a34 @comp_assoc1
+ | #o1 #o2 #a @id_neutral_right1
+ | #o1 #o2 #a @id_neutral_left1 ]