{J W P : Type} (f : J -> P) (a : J) (jr : W -> J) (jg : forall w, a = jr w) {b c : W} (p : b = c) : ap f (jg b) @ ap f (ap jr p) = ap f (jg c). Proof. apply ap_triangle. induction p. apply concat_p1. Defined.
Require Import Basics Types.Paths WildCat Join.Core HoTT.Tactics.