{A B C D} {f f' : A -> C} {g g' : B -> D} (h : f == f') (k : g == g') : functor_join f g == functor_join f' g'. Proof. srapply Join_ind_FlFr. - simpl; intros; apply ap, h. - simpl; intros; apply ap, k. - intros a b; cbn beta. lhs nrapply (functor_join_beta_jglue _ _ _ _ @@ 1). symmetry. lhs nrapply (1 @@ functor_join_beta_jglue _ _ _ _). apply join_natsq. 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.