fact: Definition join_rec {A B P : Type} (f : JoinRecData A B P) : Join A B -> P := Join_rec (jl f) (jr f) (jg f).
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core