fact: Definition functor_join_recdata {A B C D} (f : A -> C) (g : B -> D) : JoinRecData A B (Join C D) := {| jl := joinl o f; jr := joinr o g; jg := fun a b => jglue (f a) (g b); |}.
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core