open import Paths // redtt version: https://github.com/RedPRL/redtt/blob/master/library/cool/s3-to-join.red // cagda version: https://github.com/agda/cubical/blob/master/Cubical/HITs/Join/Base.agda open data join (A B : Type) | inl A | inr B | push (a : A) (b : B) : inl a = inr b