{A B P : Type} {jl' : A -> P} {jr' : B -> P} {f g : forall a b, jl' a = jr' b} (h : forall a b, f a b = g a b) : JoinRecPath (Build_JoinRecData jl' jr' f) (Build_JoinRecData jl' jr' g). Proof. snrapply Build_JoinRecPath. 1, 2: reflexivity. intros; apply equiv_p1_1q, h. 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.