{A B : Type} (P : Join A B -> Type) (P_A : forall a, P (joinl a)) (P_B : forall b, P (joinr b)) (P_g : forall a b, transport P (jglue a b) (P_A a) = (P_B b)) a b : apD (Join_ind P P_A P_B P_g) (jglue a b) = P_g a b := Pushout_ind_beta_pglue _ _ _ _ _.
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.