We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 14e39b4 commit 0751b4aCopy full SHA for 0751b4a
theories/encatI.v
@@ -3178,7 +3178,6 @@ Defined.
3178
hcomp (hu, hm) = prj2 (hu, hm) = hm
3179
(hm1 * hm2) * hm3 ~> hm1 * (hm2 * hm3)
3180
3181
-
3182
(* Double category with universal characterization of weak
3183
horizontal associativity *)
3184
HB.mixin Record IsDCat_UA T of CFunctor T := {
@@ -3193,5 +3192,4 @@ HB.mixin Record IsDCat_UA T of CFunctor T := {
3193
3192
(@HO T (@hhom T) a0 a3 hh1)
3194
}.
3195
3196
3197
*)
0 commit comments