5 lines
151 B
Text
5 lines
151 B
Text
import core
|
||
open susp smash pointed wedge prod
|
||
|
||
definition susp_product (X Y : Type*) : ⅀ (X × Y) ≃* ⅀ X ∨ (⅀ Y ∨ ⅀ (X ∧ Y)) :=
|
||
sorry
|