(P : Type) (a b : P) (p : a = b) : ap (interval_rec P a b p) seg = p. Proof. refine (cancelL (transport_const seg a) _ _ _). refine ((apD_const (interval_ind (fun _ => P) a b _) seg)^ @ _). refine (interval_ind_beta_seg (fun _ => P) _ _ _). Defined.
Require Import Basics.Overture Basics.PathGroupoids. Require Import Types.Paths.