{A B P Q : Type} (g : P -> Q) (f : JoinRecData A B P) : JoinRecData A B Q. Proof. snrapply Build_JoinRecData. - exact (g o jl f). - exact (g o jr f). - exact (fun a b => ap g (jg 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.