case nil => rfl
α : Type u
inst✝ : Category α
⊢ joinF.unitorRightOplax [] ≫ joinF.unitorRightLax [] =
    𝟙 (Prefunctor.obj (Prefunctor.obj mapF.toPrefunctor singletonF ⋙ joinF).toPrefunctor [])
no goals