fact: Definition join_rec_nat (A B : Type) {P Q : Type} (g : P -> Q) (f : JoinRecData A B P) : join_rec (joinrecdata_fun g f) $== g o join_rec f.
imports: Basics Types Cubical NullHomotopy Extensions Colimits.Pushout Truncations.Core Truncations.Connectedness Pointed.Core WildCat Spaces.Nat.Core