(A B P : Type) : joinrecdata_0gpd A B P $-> joinrecdata_0gpd B A P. Proof. snrapply Build_Morphism_0Gpd. - intros [fl fr fg]. snrapply (Build_JoinRecData fr fl). intros b a; exact (fg a b)^. - apply Build_Is0Functor. intros f g h; simpl. snrapply Build_JoinRecPath; simpl. 1, 2: intros; apply h. intros b a. square_ind g h a b. by interval_ind f a b. 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.