instMkEvalHorizontalCompBicategoryM

Lean4
instance : MkEvalHorizontalComp BicategoryM
    where
  mkEvalHorizontalCompAuxOf _
    _ := do
    throwError"not implemented"
  mkEvalHorizontalCompAuxCons _ _ _ _ _ _ _ _ _ _
    _ := do
    throwError"not implemented"
  mkEvalHorizontalCompAux'Whisker _ _ _ _ _ _ _ _ _ _
    _ := do
    throwError"not implemented"
  mkEvalHorizontalCompAux'OfWhisker _ _ _ _ _ _ _ _ _ _
    _ := do
    throwError"not implemented"
  mkEvalHorizontalCompNilNil _
    _ := do
    throwError"not implemented"
  mkEvalHorizontalCompNilCons _ _ _ _ _ _ _ _ _ _ _
    _ := do
    throwError"not implemented"
  mkEvalHorizontalCompConsNil _ _ _ _ _ _ _ _ _ _ _
    _ := do
    throwError"not implemented"
  mkEvalHorizontalCompConsCons _ _ _ _ _ _ _ _ _ _ _ _ _
    _ := do
    throwError"not implemented"
Похожие утверждения