@@ -233,7 +233,7 @@ Definition fmap_pair {A B C : Type}
233233 (F : A * B -> C) `{!Is0Functor F}
234234 {a0 a1 : A} (f : a0 $-> a1) {b0 b1 : B} (g : b0 $-> b1)
235235 : F (a0, b0) $-> F (a1, b1)
236- := fmap (a:= (a0,b0)) (b:= (a1,b1)) F (f,g).
236+ := fmap (a := (a0, b0)) (b := (a1, b1)) F (f, g).
237237
238238Definition fmap_pair_comp {A B C : Type }
239239 `{Is1Cat A, Is1Cat B, Is1Cat C}
@@ -242,12 +242,12 @@ Definition fmap_pair_comp {A B C : Type}
242242 (f : a0 $-> a1) (h : b0 $-> b1) (g : a1 $-> a2) (i : b1 $-> b2)
243243 : fmap_pair F (g $o f) (i $o h)
244244 $== fmap_pair F g i $o fmap_pair F f h
245- := fmap_comp (a:= (a0,b0)) (b:= (a1,b1)) (c:= (a2,b2)) F (f,h) (g,i).
245+ := fmap_comp (a := (a0, b0)) (b := (a1, b1)) (c := (a2, b2)) F (f, h) (g, i).
246246
247247Definition fmap2_pair {A B C : Type }
248248 `{Is1Cat A, Is1Cat B, Is1Cat C}
249249 (F : A * B -> C) `{!Is0Functor F, !Is1Functor F}
250250 {a0 a1 : A} {f f' : a0 $-> a1} (p : f $== f')
251251 {b0 b1 : B} {g g' : b0 $-> b1} (q : g $== g')
252252 : fmap_pair F f g $== fmap_pair F f' g'
253- := fmap2 F (a:= (a0,b0)) (b:= (a1,b1)) (f:= (f,g)) (g:= (f',g')) (p,q).
253+ := fmap2 F (a := (a0, b0)) (b := (a1, b1)) (f := (f, g)) (g := (f' ,g')) (p, q).
0 commit comments