{A B P : Type} (f g : Join A B -> P) (Hl : forall a, f (joinl a) = g (joinl a)) (Hr : forall b, f (joinr b) = g (joinr b)) (Hglue : forall a b, ap f (jglue a b) @ Hr b = Hl a @ ap g (jglue a b)) : f == g. Proof. snrapply Join_ind. - exact Hl. - exact Hr. - intros a b. nrapply transport_paths_FlFr'. apply Hglue. 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.