(A B : Type) : NatEquiv (joinrecdata_0gpd_fun A B) (joinrecdata_0gpd_fun B A). Proof. snrapply Build_NatEquiv. - intro P. snrapply cate_adjointify. 1, 2: apply joinrecdata_sym. 1, 2: apply joinrecdata_sym_inv. - snrapply Build_Is1Natural. intros P Q g f; simpl. bundle_joinrecpath. intros b a; simpl. symmetry; apply ap_V. 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.