(A B : Type) : NatEquiv (opyon_0gpd (Join A B)) (joinrecdata_0gpd_fun A B). Proof. snrapply Build_NatEquiv'. 1: apply join_rec_inv_nattrans. intro P. apply isequiv_0gpd_issurjinj. apply Build_IsSurjInj. - intros f; cbn in f. exists (join_rec f). apply join_rec_beta. - exact (@isinj_join_rec_inv A B P). Defined.
Require Import Basics Types. Require Import Cubical.DPath Cubical.PathSquare. Require Import NullHomotopy. Require Import Extensions. Require Import Colimits.Pushout. Require Import Truncations.Core Truncations.Connectedness. Require Import Pointed.Core. Require Import WildCat. Require Import Spaces.Nat.Core.